mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.invOrderIso.eq_1 : ∀ {G : Type u_2} [inst : Group G], Submonoid.invOrderIso = { toEquiv := Equiv.inv (Submonoid G), map_rel_iff' := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_some_get! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], a ∈ t → t.get? a = some (t.get! a)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.MorphismProperty.retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  (CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u}
        (CategoryTheory.MorphismProperty.coproducts.{w, v, u} W).pushouts).retracts ≤
    W.rlp.llp
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoalParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- The underlying modular form (via `toModularFormₗ`) of a `CuspForm` is itself a cusp form.  -/
ModularForm.CuspForm.isCuspForm_toModularFormₗ : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetOne] (f : CuspForm Γ k), (CuspForm.toModularFormₗ f).IsCuspForm
-- Mathlib.Order.CompleteLattice.Basic
Prod.fst_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : SupSet α] [inst_1 : SupSet β] (f : ι → α × β),
  (iSup f).1 = ⨆ i, (f i).1
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- This is the splitting of a short complex `S` in a balanced category induced by
a retraction of the morphism `S.f : S.X₁ ⟶ S.X₂`  -/
CategoryTheory.ShortComplex.Splitting.ofExactOfRetraction : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Balanced C] →
        (S : CategoryTheory.ShortComplex C) →
          S.Exact →
            (r : S.X₂ ⟶ S.X₁) →
              CategoryTheory.CategoryStruct.comp S.f r = CategoryTheory.CategoryStruct.id S.X₁ →
                CategoryTheory.Epi S.g → S.Splitting
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_horiz_isIso_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} [CategoryTheory.IsIso fst] [CategoryTheory.Mono g],
  CategoryTheory.CommSq fst snd f g → CategoryTheory.IsPullback fst snd f g
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.instSemilinearEquivClass : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S}
  {σ' : S →+* R} [inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ],
  SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiable.clm_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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {g : M → F₁ →L[𝕜] F₂} {f : M → F₁}, MDiff g → MDiff f → MDiff fun x => (g x) (f x)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D),
  i.isoInverseOfIsoFunctor.hom.app X =
    CategoryTheory.CategoryStruct.comp (G'.unitIso.hom.app (G.inverse.obj X))
      (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.inv.app (G.inverse.obj X)))
        (G'.inverse.map (G.counitIso.hom.app X)))
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_H : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).right.H =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instForMOfMonad : {α : Type u} → {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForM m (Std.TreeSet.Raw α cmp) α
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_neg : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Neg β] (f : α → β),
  (UniformOnFun.ofFun 𝔖) (-f) = -(UniformOnFun.ofFun 𝔖) f
-- Std.Http.Data.URI.Basic
/-- The host component.
 -/
Std.Http.URI.Builder.host : Std.Http.URI.Builder → Option Std.Http.URI.Host
-- Mathlib.Logic.Function.Basic
Function.not_injective_iff : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, ¬Function.Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b
-- Mathlib.Algebra.Group.End
MulAut.inv_apply : ∀ (M : Type u_2) [inst : Mul M] (e : MulAut M) (m : M), e⁻¹ m = (MulEquiv.symm e) m
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_le_unop_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S₁ S₂ : Subalgebra R Aᵐᵒᵖ}, S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiRing_apply : ∀ {R : Type u} {ι : Type v} {M : Type u_1} [inst : Fintype ι] [inst_1 : CommRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace M] [inst_6 : ContinuousMul R]
  [inst_7 : ContinuousSMul R M] (z : M) (m : ι → R), (ContinuousMultilinearMap.mkPiRing R ι z) m = (∏ i, m i) • z
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulLeft_one` for matrix multiplication.  -/
mulLeftLinearMap_one : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : Semiring R] [inst_3 : Semiring A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A],
  mulLeftLinearMap n R 1 = LinearMap.id
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.lowerEquivalence_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : C} {B : D} (e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B),
  (CategoryTheory.Subobject.lowerEquivalence e).unitIso = CategoryTheory.eqToIso ⋯
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} (mor₁ : obj₁ ⟶ obj₂)
  (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) {X Y : J} (φ : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.Triangle.functorMk mor₁ mor₂ mor₃).map φ).hom₃ = obj₃.map φ
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.toQuotient_map : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A), relations.toQuotient ∘ₗ relations.map = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {a b : α}, (a == b) = true → Std.DHashMap.Internal.Raw₀.Const.get? m a = Std.DHashMap.Internal.Raw₀.Const.get? m b
-- Std.Time.Date.Basic
Std.Time.instHSubOffset_5 : HSub Std.Time.Day.Offset Std.Time.Day.Offset Std.Time.Day.Offset
-- Mathlib.Data.Nat.Cast.Order.Ring
/-- Specialisation of `Nat.cast_pos'`, which seems to be easier for Lean to use.  -/
Nat.cast_pos : ∀ {α : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [Nontrivial α] {n : ℕ}, 0 < ↑n ↔ 0 < n
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_piFinsetUnion : ∀ {ι : Type u_4} {α : ι → Type u_5} {x : (i : ι) → MeasurableSpace (α i)} [inst : DecidableEq ι] {s t : Finset ι}
  (h : Disjoint s t) (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinsetUnion α h))
    ((MeasureTheory.Measure.pi fun i => μ ↑i).prod (MeasureTheory.Measure.pi fun i => μ ↑i))
    (MeasureTheory.Measure.pi fun i => μ ↑i)
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.counit_algebraMap : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (r : R),
  CoalgebraStruct.counit ((algebraMap R A) r) = r
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.coe_mk : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A →g B) (hf : Function.Injective ⇑f),
  ⇑{ toHom := f, injective' := hf } = ⇑f
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- the first row  -/
CategoryTheory.ShortComplex.SnakeInput.L₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex C
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {Z : D}
      (h :
        (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶
          Z),
      CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f)
          (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedObj F n).hom h) =
        CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom
          (CategoryTheory.CategoryStruct.comp
            ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
              ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ))
            h)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `IsConjRoot.ne_zero`, only assuming `IsDomain R`,
`IsTorsionFree R A` and `Function.Injective (algebraMap R A)` instead of `Field R`. If `y` is
a conjugate root of a nonzero element `x`, then `y` is not zero.
 -/
IsConjRoot.ne_zero_of_injective : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain S]
  [IsDomain R] [Module.IsTorsionFree R S] {x y : S},
  x ≠ 0 → IsConjRoot R x y → Function.Injective ⇑(algebraMap R S) → y ≠ 0
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplexObj_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), (Φ.shortComplexObj X).f = Φ.ι.app X
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv : ∀ {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) {M N : ↑(F.obj { as := Opposite.op S })} (φ : M ⟶ N),
  (CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv F f)
      (CategoryTheory.Presieve.Arrows.toCompatible (F.presheafHom M N) (fun i => CategoryTheory.Over.homMk (f i) ⋯)
        (F.presheafHomObjHomEquiv φ)) =
    (F.toDescentData f).map φ
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Ioc a b` and antitone on `Icc b c`, then the maximum of `f` on
`Ioc a c` is attained at `b`.  -/
isMaxOn_Ioc_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b c : α} {f : α → β},
  MonotoneOn f (Set.Ioc a b) → AntitoneOn f (Set.Icc b c) → IsMaxOn f (Set.Ioc a c) b
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_top : ∀ {α : Type u_1} [Nontrivial α] (u : α), ⊤.eccent u = 1
-- Mathlib.Tactic.TFAE
/-- See `letPatDecl`. E.g. `⟨mp, mpr⟩ : 1 ↔ 3 := term`.  -/
Mathlib.Tactic.TFAE.Parser.tfaeHavePatDecl : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (X : P.I), (P.toCostructuredArrow.obj X).left = P.F.obj X
-- Init.Data.Option.Lemmas
Option.get_of_mem : ∀ {α : Type u_1} {a : α} {o : Option α} (h : o.isSome = true), a ∈ o → o.get h = a
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.contained_eq_proj : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  Profinite.NobelingProof.contained C o → C = Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o
-- Mathlib.Topology.Algebra.Group.Basic
/-- Negation in a topological group as a homeomorphism.  -/
Homeomorph.neg : (G : Type u_1) → [inst : TopologicalSpace G] → [inst_1 : InvolutiveNeg G] → [ContinuousNeg G] → G ≃ₜ G
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Polynomial.Chebyshev.complex_ofReal_eval_U : ∀ (x : ℝ) (n : ℤ), ↑(Polynomial.eval x (Polynomial.Chebyshev.U ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.U ℂ n)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
MeasureTheory.AEStronglyMeasurable.im : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → 𝕜},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => RCLike.im (f x)) μ
-- Mathlib.Computability.Primrec.Basic
Primrec.option_isSome : ∀ {α : Type u_1} [inst : Primcodable α], Primrec Option.isSome
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.instAddCommGroupQuot : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] → AddCommGroup (AddCommGrpCat.Colimits.Quot F)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `coeq₃Hom f g h`, for morphisms `f g h : j₁ ⟶ j₂`, is an arbitrary choice of morphism
`j₂ ⟶ coeq₃ f g h` such that `coeq₃_condition₁`, `coeq₃_condition₂` and `coeq₃_condition₃`
are satisfied. Its existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.coeq₃Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] →
      {j₁ j₂ : C} → (f g h : j₁ ⟶ j₂) → j₂ ⟶ CategoryTheory.IsFiltered.coeq₃ f g h
-- Std.Http.Data.Request
/-- Inserts a typed extension value into the request being built.
 -/
Std.Http.Request.Builder.extension : {α : Type u_1} → Std.Http.Request.Builder → [TypeName α] → α → Std.Http.Request.Builder
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfectCompl.isCompl_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R} [inst_5 : p.IsPerfPair] {U : Submodule R M}
  {V : Submodule R N}, p.IsPerfectCompl U V → IsCompl V (Submodule.map (↑p.flip.toPerfPair.symm) U.dualAnnihilator)
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
/-- This lemma matches more generally than
`Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk` when using `rw ← `.  -/
Finset.Nat.sum_antidiagonal_eq_sum_range_succ : ∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
  ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij.1 ij.2 = ∑ k ∈ Finset.range n.succ, f k (n - k)
-- Init.Core
LawfulSingleton.mk : ∀ {α : Type u} {β : Type v} [inst : EmptyCollection β] [inst_1 : Insert α β] [inst_2 : Singleton α β],
  (∀ (x : α), insert x ∅ = {x}) → LawfulSingleton α β
-- Mathlib.Data.Fin.Basic
Fin.sub_ne_last_of_ne_last_of_le : ∀ {n : ℕ} {a b : Fin (n + 1)}, a ≠ Fin.last n → b ≤ a → a - b ≠ Fin.last n
-- Std.Data.ByteSlice
ByteSlice.instBEq : BEq ByteSlice
-- Mathlib.Data.Finset.Lattice.Fold
Multiset.map_finset_sup : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq α] [inst_1 : DecidableEq β] (s : Finset γ)
  (f : γ → Multiset β) (g : β → α), Function.Injective g → Multiset.map g (s.sup f) = s.sup (Multiset.map g ∘ f)
-- Mathlib.Data.W.Constructions
WType.leftInverse_list : ∀ (γ : Type u), Function.LeftInverse (WType.ofList γ) (WType.toList γ)
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_emod_right : ∀ (a b : ℤ), a * b % a = 0
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
rothNumberNat_zero : rothNumberNat 0 = 0
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebra_equiv_of_iso_monads_comp_forget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ⟶ T₂),
  (CategoryTheory.Monad.algebraFunctorOfMonadHom h).comp T₁.forget = T₂.forget
-- Mathlib.Algebra.Group.ForwardDiff
/-- **Alias** of `fwdDiff_finsetSum`. -/
fwdDiff_finset_sum : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) {α : Type u_3} (s : Finset α)
  (f : α → M → G), fwdDiff h (∑ k ∈ s, f k) = ∑ k ∈ s, fwdDiff h (f k)
-- Mathlib.Algebra.BigOperators.Finprod
/-- If the additive supports of `f` and `g` are finite, then the sum of `f i + g i`
equals the sum of `f i` plus the sum of `g i`.  -/
finsum_add_distrib : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f g : α → M},
  Function.HasFiniteSupport f →
    Function.HasFiniteSupport g → ∑ᶠ (i : α), (f i + g i) = ∑ᶠ (i : α), f i + ∑ᶠ (i : α), g i
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmaKey.type : Lean.Meta.AuxLemmaKey → Lean.Expr
-- Std.Tactic.Do.Syntax
/-- Like `mspec`, but does not attempt slight simplification and closing of trivial sub-goals.
`mspec $spec` is roughly (the set of simp lemmas below might not be up to date)
```
mspec_no_simp $spec
all_goals
  ((try simp only [SPred.true_intro_simp, SPred.apply_pure]);
   (try mpure_intro; trivial))
```
 -/
Lean.Parser.Tactic.mspecNoSimp : Lean.ParserDescr
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.StateStack.mk.injEq : ∀ {α β σ : Type} (stateStack : List (Lean.ScopedEnvExtension.State σ))
  (scopedEntries : Lean.ScopedEnvExtension.ScopedEntries β) (newEntries : List (Lean.ScopedEnvExtension.Entry α))
  (stateStack_1 : List (Lean.ScopedEnvExtension.State σ)) (scopedEntries_1 : Lean.ScopedEnvExtension.ScopedEntries β)
  (newEntries_1 : List (Lean.ScopedEnvExtension.Entry α)),
  ({ stateStack := stateStack, scopedEntries := scopedEntries, newEntries := newEntries } =
      { stateStack := stateStack_1, scopedEntries := scopedEntries_1, newEntries := newEntries_1 }) =
    (stateStack = stateStack_1 ∧ scopedEntries = scopedEntries_1 ∧ newEntries = newEntries_1)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_congr_l : ∀ {σs : List (Type u)} {P P' Q : Std.Do.SPred σs}, (P ⊣⊢ₛ P') → P ∧ Q ⊣⊢ₛ P' ∧ Q
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Order.Filter.Bases.Basic
/-- Constructs a filter from an indexed family of sets satisfying `IsBasis`.  -/
Filter.IsBasis.filter : {α : Type u_1} → {ι : Sort u_4} → {p : ι → Prop} → {s : ι → Set α} → Filter.IsBasis p s → Filter α
-- Batteries.Data.Array.Pairwise
Array.pairwise_empty : ∀ {α : Type u_1} {R : α → α → Prop}, Array.Pairwise R #[]
-- Init.Data.Int.Cooper
Int.Cooper.resolve_left_inv : ℤ → ℤ → ℤ → ℤ
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.global.sizeOf_spec : ∀ (m : Aesop.GlobalRuleSetMember), sizeOf (Aesop.LocalRuleSetMember.global m) = 1 + sizeOf m
-- Mathlib.Data.WSeq.Defs
/-- Replace the `n`th element of `s` with `a`.  -/
Stream'.WSeq.updateNth : {α : Type u} → Stream'.WSeq α → ℕ → α → Stream'.WSeq α
-- Mathlib.Data.Int.Init
/-- If `n > 0` then `m` is not divisible by `n` iff it is between `n * k` and `n * (k + 1)`
for some `k`.  -/
Int.exists_lt_and_lt_iff_not_dvd : ∀ {n : ℤ} (m : ℤ), 0 < n → ((∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬n ∣ m)
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfFinset.eq_1 : ∀ {ι : Type u_1} (a s : ι → ℕ) (t : Finset ι) (hs : ∀ i ∈ t, s i ≠ 0)
  (pp : (↑t).Pairwise (Function.onFun Nat.Coprime s)),
  Nat.chineseRemainderOfFinset a s t hs pp = Nat.chineseRemainderOfMultiset a s ⋯ ⋯ ⋯
-- Mathlib.Topology.Order.HullKernel
/-- When `T` is order generating, the `kernel` and the `hull` form a Galois insertion
 -/
PrimitiveSpectrum.gi : {α : Type u_1} →
  [inst : CompleteLattice α] →
    {T : Set α} →
      PrimitiveSpectrum.OrderGenerates T →
        GaloisInsertion (⇑OrderDual.toDual ∘ PrimitiveSpectrum.kernel) (PrimitiveSpectrum.hull T ∘ ⇑OrderDual.ofDual)
-- Mathlib.Data.Finset.Prod
Finset.diag_card : ∀ {α : Type u_1} (s : Finset α), s.diag.card = s.card
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.totalDegree_neg : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (a : MvPolynomial σ R), (-a).totalDegree = a.totalDegree
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.mk.inj : ∀ {𝕜 : Type u} {A : Type v} {inst : NontriviallyNormedField 𝕜} {inst_1 : NonUnitalNormedRing A}
  {inst_2 : NormedSpace 𝕜 A} {inst_3 : SMulCommClass 𝕜 A A} {inst_4 : IsScalarTower 𝕜 A A}
  {toProd : (A →L[𝕜] A) × (A →L[𝕜] A)} {central : ∀ (x y : A), toProd.2 x * y = x * toProd.1 y}
  {toProd_1 : (A →L[𝕜] A) × (A →L[𝕜] A)} {central_1 : ∀ (x y : A), toProd_1.2 x * y = x * toProd_1.1 y},
  { toProd := toProd, central := central } = { toProd := toProd_1, central := central_1 } → toProd = toProd_1
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.zero_eq_zero' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C},
  ⟦CategoryTheory.Over.mk 0⟧ = ⟦CategoryTheory.Over.mk 0⟧