mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.fstPiMap_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (b : J.R),
  CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.Limits.Pi.π I.right b) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (J.fst b)) (I.fst b)
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
/-- Explicit formula for the derivative of the complex Gamma function at positive integers, in
terms of harmonic numbers and the Euler-Mascheroni constant `γ`.  -/
Complex.deriv_Gamma_nat : ∀ (n : ℕ), deriv Complex.Gamma (↑n + 1) = ↑n.factorial * (-↑Real.eulerMascheroniConstant + ↑(harmonic n))
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_apply : ∀ {n : Type u_3} {α : Type v} (A : Matrix n n α) (i : n), A.diag i = A i i
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.iterated_mateEquiv_conjugateEquiv_symm : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {F₁ : CategoryTheory.Functor A C} {U₁ : CategoryTheory.Functor C A}
  {F₂ : CategoryTheory.Functor B D} {U₂ : CategoryTheory.Functor D B} {L₁ : CategoryTheory.Functor A B}
  {R₁ : CategoryTheory.Functor B A} {L₂ : CategoryTheory.Functor C D} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁)
  (adj₂ : L₂ ⊣ R₂) (adj₃ : F₁ ⊣ U₁) (adj₄ : F₂ ⊣ U₂) (α : CategoryTheory.TwoSquare U₂ R₂ R₁ U₁),
  (CategoryTheory.mateEquiv adj₁ adj₂).symm ((CategoryTheory.mateEquiv adj₄ adj₃).symm α) =
    ((CategoryTheory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans
        (CategoryTheory.TwoSquare.equivNatTrans F₁ L₁ L₂ F₂).symm)
      α
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedMonoid.enorm_mul_le : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ESeminormedMonoid E] (x y : E), ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.nerveEquiv_symm_apply_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : C) (x : Fin 1),
  (SSet.OneTruncation₂.nerveEquiv.symm f).obj x = f
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusEquiv_apply : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [inst_1 : CharP R p] [inst_2 : PerfectRing R p],
  ⇑(WittVector.frobeniusEquiv p R) = ⇑WittVector.frobenius
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- Arbitrary coloring with two colors for a forest  -/
SimpleGraph.IsAcyclic.coloringTwo : {V : Type u_1} → {G : SimpleGraph V} → G.IsAcyclic → G.Coloring (Fin 2)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.ringHom_ext_iff : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} {S : Type v} [inst_1 : I.IsTwoSided] [inst_2 : NonAssocSemiring S]
  {f g : R ⧸ I →+* S}, f = g ↔ f.comp (Ideal.Quotient.mk I) = g.comp (Ideal.Quotient.mk I)
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIio : {α : Type u_1} → [inst : Preorder α] → {b x : α} → [Decidable (x < b)] → Decidable (x ∈ Set.Iio b)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.leadingCoeff_toLex_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : LinearOrder σ] (r : R),
  AddMonoidAlgebra.leadingCoeff (⇑toLex) (MvPolynomial.C r) = r
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toLinearMap_eq_coe : ∀ {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 σ' σ] {e : M ≃ₛₗ[σ] M₂}, ↑e = ↑e
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
MonoidAlgebra.mem_smulAntidiagonal_of_group : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : Group G] [inst_1 : MulAction G P]
  [inst_2 : Semiring R] [inst_3 : Zero V] (f : MonoidAlgebra R G) (x : P → V) (p : P) (gh : G × P),
  gh ∈ Finset.SMulAntidiagonal p ⋯ ↔ f.coeff gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = gh.1⁻¹ • p
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instZero.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : Zero β], MeasureTheory.AEEqFun.instZero = { zero := MeasureTheory.AEEqFun.const α 0 }
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.map_dirac : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [MeasurableSingletonClass α]
  [MeasurableSingletonClass β] {f : α → β} (a : α),
  MeasureTheory.Measure.map f (MeasureTheory.Measure.dirac a) = MeasureTheory.Measure.dirac (f a)
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.simpAppUsingCongr.visit : Lean.Expr → Lean.Meta.Simp.Config → Array Lean.Meta.ParamInfo → Lean.Expr → ℕ → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.isContained_congr_right : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (e₂ : B ≃g C), A.IsContained B ↔ A.IsContained C
-- Mathlib.Analysis.Normed.Order.UpperLower
IsUpperSet.exists_subset_ball : ∀ {ι : Type u_2} [inst : Fintype ι] {s : Set (ι → ℝ)} {x : ι → ℝ} {δ : ℝ},
  IsUpperSet s →
    x ∈ closure s →
      0 < δ → ∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β),
  FreeAddGroup.map f = AddMonoidHom.mk' (Quot.map (List.map fun x => (f x.1, x.2)) ⋯) ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget.lhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w → aig.RefVec w
-- Mathlib.Algebra.Symmetrized
SymAlg.instNeg : {α : Type u_1} → [Neg α] → Neg αˢʸᵐ
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.mem_cylinder_firstDiff : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), x ∈ PiNat.cylinder y (PiNat.firstDiff x y)
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
Liouville.eq_1 : ∀ (x : ℝ), Liouville x = ∀ (n : ℕ), ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformly.hasProdLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], MultipliableLocallyUniformly f → HasProdLocallyUniformly f fun x => ∏' (i : ι), f i x
-- Mathlib.Topology.MetricSpace.Cover
/-- A closed set in a proper metric space which admits a compact cover is compact.  -/
Metric.IsCover.isCompact : ∀ {X : Type u_1} [inst : MetricSpace X] [ProperSpace X] {ε : NNReal} {s N : Set X},
  Metric.IsCover ε s N → IsClosed s → IsCompact N → IsCompact s
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.opEquiv_symm_apply : ∀ {M : Type u_2} [inst : AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ), (RelIso.symm AddSubmonoid.opEquiv) x = x.unop
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mk.injEq : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (toMultilinearMap : MultilinearMap R M₁ M₂) (cont : Continuous toMultilinearMap.toFun)
  (toMultilinearMap_1 : MultilinearMap R M₁ M₂) (cont_1 : Continuous toMultilinearMap_1.toFun),
  ({ toMultilinearMap := toMultilinearMap, cont := cont } =
      { toMultilinearMap := toMultilinearMap_1, cont := cont_1 }) =
    (toMultilinearMap = toMultilinearMap_1)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Compose the quadratic map with a linear function on the right.  -/
QuadraticMap.comp : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      {P : Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] →
                  [inst_5 : AddCommMonoid P] →
                    [inst_6 : Module R P] → QuadraticMap R N P → (M →ₗ[R] N) → QuadraticMap R M P
-- Mathlib.Data.Sign.Defs
SignType.enumList_nodup : SignType.enumList.Nodup
-- Mathlib.Order.PiLex
Pi.toColex_update_le_self_iff : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedGT ι], toColex (Function.update x i a) ≤ toColex x ↔ a ≤ x i
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
/-- SGA3 XXI Prop. 2.3.1  -/
RootPairing.coxeterWeightIn_le_four : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Finite ι]
  (S : Type u_5) [inst_6 : CommRing S] [inst_7 : LinearOrder S] [IsStrictOrderedRing S] [inst_9 : Algebra S R]
  [FaithfulSMul S R] [inst_11 : Module S M] [IsScalarTower S R M] [inst_13 : P.IsValuedIn S] (i j : ι),
  P.coxeterWeightIn S i j ≤ 4
-- Lean.Syntax
Lean.Syntax.instBEqRange : BEq Lean.Syntax.Range
-- Mathlib.Data.Set.Basic
Set.ofPred_inj : ∀ {α : Type u} {p q : α → Prop}, {x | p x} = {x | q x} ↔ p = q
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.RevMatchesAt.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  (∃ startPos, String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos pos) →
    String.Slice.Pattern.Model.RevMatchesAt pat pos
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_injective : ∀ (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S], Function.Injective ↑R
-- Init.Data.Rat.Basic
Rat.instMin : Min ℚ
-- Mathlib.Algebra.Group.Equiv.Defs
MonoidHom.toMulEquiv.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (g : N →* M)
  (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N),
  f.toMulEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.diff_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ t₄ : Std.TreeMap.Raw α β cmp},
  t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ \ t₂).Equiv (t₃ \ t₄)
-- Init.PropLemmas
dite_eq_right_iff : ∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x : p → α} {y : α},
  (if h : p then x h else y) = y ↔ ∀ (h : p), x h = y
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Walk.IsCycle.isCycles_spanningCoe_toSubgraph : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → p.toSubgraph.spanningCoe.IsCycles
-- Mathlib.Order.Bounds.Basic
/-- A set `s` is not bounded below if and only if for each `x` there exists `y ∈ s` that is less
than `x`. A version for preorders is called `not_bddBelow_iff'`.  -/
not_bddBelow_iff : ∀ {α : Type u_4} [inst : LinearOrder α] {s : Set α}, ¬BddBelow s ↔ ∀ (x : α), ∃ y ∈ s, y < x
-- Mathlib.Data.Finset.Option
Finset.eraseNone_eq_biUnion : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset (Option α)), Finset.eraseNone s = s.biUnion Option.toFinset
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.Trace.verbose : Lean.Lsp.Trace
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensOptions.mk.injEq : ∀ (legend : Lean.Lsp.SemanticTokensLegend) (range full : Bool) (legend_1 : Lean.Lsp.SemanticTokensLegend)
  (range_1 full_1 : Bool),
  ({ legend := legend, range := range, full := full } = { legend := legend_1, range := range_1, full := full_1 }) =
    (legend = legend_1 ∧ range = range_1 ∧ full = full_1)
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Adjunction.rightOp_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Dᵒᵖ C} (a : F.rightOp ⊣ G),
  a.rightOp = (CategoryTheory.opOpEquivalence D).symm.toAdjunction.comp a.op
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `M ⊗ -` is an exact functor.
See `Module.Flat.iff_lTensor_exact'` to generalize the universe of
`N, N', N''` to any universe that is higher than `R` and `M`.  -/
Module.Flat.iff_lTensor_exact : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔
    ∀ ⦃N N' N'' : Type (max u v)⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : AddCommGroup N'']
      [inst_6 : Module R N] [inst_7 : Module R N'] [inst_8 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.denote_toNormPoly : ∀ (ctx : Nat.Internal.Linear.Context) (c : Nat.Internal.Linear.ExprCnstr),
  Nat.Internal.Linear.PolyCnstr.denote ctx c.toNormPoly = Nat.Internal.Linear.ExprCnstr.denote ctx c
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Relations.directSum_R : ∀ {A : Type u} [inst : Ring A] {ι : Type w} (relations : ι → Module.Relations A),
  (Module.Relations.directSum relations).R = ((i : ι) × (relations i).R)
-- Mathlib.Analysis.Normed.Order.Lattice
isClosed_nonneg : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  IsClosed {x | 0 ≤ x}
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.isSuccLimit_opow_left : ∀ {a b : Ordinal.{u_1}}, Order.IsSuccLimit a → b ≠ 0 → Order.IsSuccLimit (a ^ b)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_zero : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ↑0 = 0
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.hsmul.eq_1 : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : Monoid M] {S : Submonoid M} [inst_1 : OreLocalization.OreSet S]
  [inst_2 : MulAction M X] [inst_3 : SMul R M] (c : R),
  OreLocalization.hsmul c =
    OreLocalization.liftExpand (fun m s => OreLocalization.oreNum (c • 1) s • m /ₒ OreLocalization.oreDenom (c • 1) s) ⋯
-- Mathlib.Topology.Algebra.MulAction
Specializes.vadd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X] {a b : M} {x y : X}, a ⤳ b → x ⤳ y → (a +ᵥ x) ⤳ (b +ᵥ y)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.instStructureConstantsOnElemWithConstants : {L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] →
      (A : Set M) →
        {N : Type w'} →
          [inst_1 : L.Structure N] →
            (f : L.Embedding M N) → (FirstOrder.Language.constantsOn ↑A).Structure (f.withConstants A)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mul_div_mul_comm_of_dvd_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] {a b c d : R}, c ∣ a → d ∣ b → a * b / (c * d) = a / c * (b / d)
-- Init.Tactics
/-- `as_aux_lemma => tac` does the same as `tac`, except that it wraps the resulting expression
into an auxiliary lemma. In some cases, this significantly reduces the size of expressions
because the proof term is not duplicated.
 -/
Lean.Parser.Tactic.as_aux_lemma : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Prod
AlgEquiv.prodCongr_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_5} {T : Type u_6} {A : Type u_7} {B : Type u_8}
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring S] [inst_4 : Semiring T] [inst_5 : Algebra R S]
  [inst_6 : Algebra R T] [inst_7 : Algebra R A] [inst_8 : Algebra R B] (l : S ≃ₐ[R] A) (r : T ≃ₐ[R] B) (x : A × B),
  (l.prodCongr r).symm x = ((↑l).prodCongr ↑r).symm x
-- Mathlib.Data.Rel
SetRel.dom_univ : ∀ {α : Type u_1} {β : Type u_2} [Nonempty β], SetRel.dom Set.univ = Set.univ
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell_two : Nat.bell 2 = 2
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rankMax.eq_1 : ∀ (self : Batteries.UnionFind), self.rankMax = Array.foldr (fun x => max x.rank) 0 self.arr + 1
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- **Alias** of `MeasureTheory.sdiff_null_ae_eq_self`. -/
MeasureTheory.diff_null_ae_eq_self : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, μ t = 0 → s \ t =ᵐ[μ] s
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.instZero : ∀ (p : ENNReal), p.HolderTriple 0 0
-- Lean.Level
Lean.Level.PP.Result.leaf.injEq : ∀ (a a_1 : Lean.Name), (Lean.Level.PP.Result.leaf a = Lean.Level.PP.Result.leaf a_1) = (a = a_1)
-- Init.Notation
/-- `Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`. -/
«term¬_» : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.ext_iff_degree_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ},
  p.degree ≤ ↑n → q.degree ≤ ↑n → (p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i)
-- Mathlib.NumberTheory.NumberField.ClassNumber
NumberField.RingOfIntegers.instFintypeClassGroup : (K : Type u_1) → [inst : Field K] → [NumberField K] → Fintype (ClassGroup (NumberField.RingOfIntegers K))
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.nsmul_left : ∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), AddCommute (n • a) b
-- Mathlib.Analysis.Calculus.ParametricIntegral
/-- Differentiation under integral of `x ↦ ∫ x in a..b, F x t` at a given point `x₀ ∈ (a,b)`,
assuming `F x₀` is integrable on `(a,b)`, that `x ↦ F x t` is Lipschitz on a neighborhood of `x₀`
for almost every `t` (with a neighborhood independent of `t`) with integrable Lipschitz bound,
and `F x` is a.e.-measurable for `x` in a possibly smaller neighborhood of `x₀`.  -/
hasFDerivAt_integral_of_dominated_loc_of_lip_interval : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_4} [inst_2 : NormedAddCommGroup H]
  {x₀ : H} {s : Set H} [inst_3 : NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[ℝ] E}
  {a b : ℝ} {bound : ℝ → ℝ},
  s ∈ nhds x₀ →
    (∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
      IntervalIntegrable (F x₀) μ a b →
        MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b)) →
          (∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) →
            IntervalIntegrable bound μ a b →
              (∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), HasFDerivAt (fun x => F x t) (F' t) x₀) →
                IntervalIntegrable F' μ a b ∧
                  HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMap_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
  [inst_4 : S₃.HasLeftHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) {Z : C} (h : S₃.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ₂) h)
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
/-- Let `A` be an `R`-algebra.
`𝔭 : Spec R` is in the image of `Z(I) ∩ D(f) ⊆ Spec S`
if and only if `f` is not nilpotent on `κ(𝔭) ⊗ A ⧸ I`.  -/
PrimeSpectrum.mem_image_comap_zeroLocus_sdiff : ∀ {R : Type u_2} {A : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (f : A) (s : Set A)
  (x : PrimeSpectrum R),
  x ∈ PrimeSpectrum.comap (algebraMap R A) '' (PrimeSpectrum.zeroLocus s \ PrimeSpectrum.zeroLocus {f}) ↔
    ¬IsNilpotent ((algebraMap A (TensorProduct R (A ⧸ Ideal.span s) x.asIdeal.ResidueField)) f)
-- Std.Async.System
Std.Async.System.instInhabitedGroupInfo : Inhabited Std.Async.System.GroupInfo
-- Mathlib.Order.Interval.Set.InitialSeg
Set.principalSegIioIicOfLE_apply : ∀ {α : Type u_1} [inst : Preorder α] {i j : α} (h : i ≤ j) (k : ↑(Set.Iio i)),
  (Set.principalSegIioIicOfLE h).toRelEmbedding k = ⟨↑k, ⋯⟩
-- Mathlib.Data.List.Pairwise
List.Pairwise.set_pairwise : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l → ∀ [Std.Symm R], {x | x ∈ l}.Pairwise R
-- Lean.Server.GoTo
Lean.Server.GoToKind.definition : Lean.Server.GoToKind
-- Lean.MonadEnv
Lean.isInductive : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.nat_mul_sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α] [inst_1 : Ring β],
  Function.Antiperiodic f c → ∀ (n : ℕ), f (↑n * c - x) = (-1) ^ n * f (-x)
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.pf_div_c : ∀ {α : Type u_1} {a b : α} [inst : Div α], a = b → ∀ (c : α), a / c = b / c
-- Mathlib.CategoryTheory.Subobject.Presheaf
Subobject.presheaf_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X Y : Cᵒᵖ}
  (f : X ⟶ Y), (Subobject.presheaf C).map f = TypeCat.ofHom (CategoryTheory.Subobject.pullback f.unop).obj
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanILeanHeaderSetupInfoParams.mk.inj : ∀ {version : ℕ} {isSetupFailure : Bool} {directImports : Array Lean.Lsp.ImportInfo} {version_1 : ℕ}
  {isSetupFailure_1 : Bool} {directImports_1 : Array Lean.Lsp.ImportInfo},
  { version := version, isSetupFailure := isSetupFailure, directImports := directImports } =
      { version := version_1, isSetupFailure := isSetupFailure_1, directImports := directImports_1 } →
    version = version_1 ∧ isSetupFailure = isSetupFailure_1 ∧ directImports = directImports_1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
atBot_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  [ClosedIicTopology α], Filter.atBot.IsMeasurablyGenerated
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the forward direction of `isOfFinOrder_iff_pow_eq_one`. -/
IsOfFinOrder.exists_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinOrder x → ∃ n, 0 < n ∧ x ^ n = 1
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Prod.instIsUniformGroup : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] [inst_2 : UniformSpace G] [hG : IsUniformGroup G]
  [inst_3 : UniformSpace H] [hH : IsUniformGroup H], IsUniformGroup (G × H)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Multiset.card_le_card_toFinset_add_one_iff : ∀ {α : Type u_2} [inst : DecidableEq α] {m : Multiset α},
  m.card ≤ m.toFinset.card + 1 ↔
    ∀ (x y : α), 1 < Multiset.count x m → 1 < Multiset.count y m → x = y ∧ Multiset.count x m = 2