mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PrincipalIdealDomain
IsPrincipalIdealRing.of_isNoetherianRing_of_isBezout : ∀ {R : Type u} [inst : Semiring R] [IsNoetherianRing R] [IsBezout R], IsPrincipalIdealRing R
-- Lean.DocString.Types
Lean.Doc.ListItem.mk.inj : ∀ {α : Type u} {contents contents_1 : Array α},
  { contents := contents } = { contents := contents_1 } → contents = contents_1
-- Mathlib.Order.Disjoint
isCompl_bot_top : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], IsCompl ⊥ ⊤
-- Mathlib.Algebra.Module.ULift
ULift.addAction' : {R : Type u} → {M : Type v} → [inst : AddMonoid R] → [AddAction R M] → AddAction R (ULift.{u_1, v} M)
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
/-- Given a measure `μ` and an integrable function `f`, `μ.withDensityᵥ f` is
the vector measure which maps the set `s` to `∫ₛ f ∂μ`.  -/
MeasureTheory.Measure.withDensityᵥ : {α : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → {m : MeasurableSpace α} → MeasureTheory.Measure α → (α → E) → MeasureTheory.VectorMeasure α E
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_biUnion_iff : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) {t : Set ι},
  t.Countable →
    ∀ (p : α → Prop), (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.comp_adj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {X Y Z : CategoryTheory.Bicategory.Adj B}
  (f : CategoryTheory.Bicategory.Adj.Hom X.obj Y.obj) (g : CategoryTheory.Bicategory.Adj.Hom Y.obj Z.obj),
  (CategoryTheory.CategoryStruct.comp f g).adj = f.adj.comp g.adj
-- Mathlib.Tactic.Linter.Whitespace
/-- The distance to the end of the source string, as number of string positions  -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.srcEndPos : Mathlib.Linter.FormatError✝ → String.Pos.Raw
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right]
  {K₁ K₂ :
    CategoryTheory.Limits.Cofork
      (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))
      (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))}
  (f : K₁ ⟶ K₂), (I.multicoforkEquivSigmaCofork.inverse.map f).hom = f.hom
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.findSplit?.find?.unsafe_1 : Lean.Meta.SplitKind → Lean.ExprSet → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Tactic.NormNum.Prime
/-- A predicate representing partial progress in a proof of `minFac`.  -/
Mathlib.Meta.NormNum.MinFacHelper : ℕ → ℕ → Prop
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx?.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.instIsFiniteTypeLocalGeneratorsDataOfIsFinitePresentation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.QuasicoherentData) [q.IsFinitePresentation], q.localGeneratorsData.IsFiniteType
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁) [inst_5 : vK.HasExtension vL]
  {x : ↥vK.valuationSubring},
  (algebraMap ↥vK.valuationSubring ↥vL.valuationSubring) x ∈ IsLocalRing.maximalIdeal ↥vL.valuationSubring ↔
    x ∈ IsLocalRing.maximalIdeal ↥vK.valuationSubring
-- Mathlib.Algebra.Notation.Prod
Prod.swap_zero : ∀ {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N], Prod.swap 0 = 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsNormal.conj' : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  S.IsNormal →
    ∀ {c d : C} (p : d ⟶ c) {γ : c ⟶ c},
      γ ∈ S.arrows c c →
        CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp γ (CategoryTheory.Groupoid.inv p)) ∈
          S.arrows d d
-- Mathlib.Algebra.Group.Ext
CancelMonoid.toLeftCancelMonoid_injective : ∀ {M : Type u}, Function.Injective (@CancelMonoid.toLeftCancelMonoid M)
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
/-- **Alias** of `AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE`. -/
AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.FormallyUnramified f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FormallyUnramified
-- Init.Prelude
/-- Use the indexing notation `a[i]` instead.

Access an element from an array without needing a runtime bounds checks,
using a `Nat` index and a proof that it is in bounds.

This function does not use `get_elem_tactic` to automatically find the proof that
the index is in bounds. This is because the tactic itself needs to look up values in
arrays.
 -/
Array.getInternal : {α : Type u} → (a : Array α) → (i : ℕ) → i < a.size → α
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.map_mulEquiv : ∀ {B : Type u_1} {W : Type u_3} {H : Type u_4} [inst : Group W] [inst_1 : Group H] {M : CoxeterMatrix B}
  (cs : CoxeterSystem M W) (e : W ≃* H), (cs.map e).mulEquiv = e.symm.trans cs.mulEquiv
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHomotopy.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {φ₁ φ₂ : F ⟶ G} (ho : Homotopy φ₁ φ₂),
  CochainComplex.HomComplex.Cochain.ofHomotopy ho = CochainComplex.HomComplex.Cochain.mk fun p q x => ho.hom p q
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.AbsolutelyContinuous.comp_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  (μ : MeasureTheory.Measure α),
  (∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) → (μ.bind ⇑κ).AbsolutelyContinuous (μ.bind ⇑η)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trCont.eq_3 : ∀ (a : List ℕ) (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.trCont (Turing.ToPartrec.Cont.cons₂ a k) = (Turing.PartrecToTM2.trCont k).cons₂
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.degree_basisDivisor_of_ne : ∀ {F : Type u_1} [inst : Field F] {x y : F}, x ≠ y → (Lagrange.basisDivisor x y).degree = 1
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_one_iff`. -/
Filter.IsBoundedUnder.isBigO_one : ∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] {f : α → E} {l : Filter α}
  [inst_2 : One F] [NormOneClass F],
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x‖) → f =O[l] fun _x => 1
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instGroupOfIsTopologicalGroup : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Group β] → [IsTopologicalGroup β] → Group C(α, β)
-- Init.Data.String.Iterator
/-- Checks whether the iterator is past its string's last character.
 -/
String.Legacy.Iterator.atEnd : String.Legacy.Iterator → Bool
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- A copy of `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`
for the canonical spelling of the equivalence.  -/
PiLp.volume_preserving_ofLp : ∀ (ι : Type u_4) [inst : Fintype ι],
  MeasureTheory.MeasurePreserving WithLp.ofLp MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_le_sqrt_iff' : ∀ {x y : ℝ}, 0 < x → (√x ≤ √y ↔ x ≤ y)
-- Mathlib.Analysis.Normed.Group.Constructions
IsGreatest.pi_norm' : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedGroup E] [Nonempty ι] (f : ι → E),
  IsGreatest (Set.range fun x => ‖f x‖) ‖f‖
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- `C` has all wide pushouts for any Finite `J`  -/
CategoryTheory.Limits.HasFiniteWidePushouts.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteWidePushouts C]
  (J : Type) [Finite J], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- A specialization of the spectral mapping theorem for polynomials in a Banach algebra over `ℂ`
to monic monomials.  -/
spectrum.map_pow : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) (n : ℕ),
  spectrum ℂ (a ^ n) = (fun x => x ^ n) '' spectrum ℂ a
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
/-- The Radon-Nikodym derivative `∂(μ.map g)/∂(ν.map g)` of the pushforward of measures by
a function `g : 𝓧 → 𝓨` evaluated at `g x` is a.e.-equal to the conditional expectation of `∂μ/∂ν`
with respect to the comap by `g` of the sigma-algebra on `𝓨`.

See `rnDeriv_map` for the same statement, but with a.e. equality with respect to the measure `ν`.  -/
MeasureTheory.rnDeriv_map_ae_eq_trim : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ],
  μ.AbsolutelyContinuous ν →
    ∀ {g : 𝓧 → 𝓨} (hg : Measurable g) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g ν)],
      (fun a => (MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g a)) =ᵐ[ν.trim ⋯]
        ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- If `L` is a finer precoverage than `K`, any `0`-hypercover wrt. `K` is in particular
a `0`-hypercover wrt. to `L`.  -/
CategoryTheory.Precoverage.ZeroHypercover.weaken : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K L : CategoryTheory.Precoverage C} → {X : C} → K.ZeroHypercover X → K ≤ L → L.ZeroHypercover X
-- Std.Data.HashMap.Basic
Std.HashMap.instRepr : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → [Repr α] → [Repr β] → Repr (Std.HashMap α β)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.degLex_def : ∀ {α : Type u_1} {r : α → α → Prop} {s : ℕ → ℕ → Prop} {a b : α →₀ ℕ},
  Finsupp.DegLex r s a b ↔ Prod.Lex s (Finsupp.Lex r s) (Finsupp.degree a, a) (Finsupp.degree b, b)
-- Mathlib.Logic.Function.Basic
Function.Injective.isLinearOrder_onFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) {f : α → β},
  Function.Injective f → ∀ [IsLinearOrder β r], IsLinearOrder α (Function.onFun r f)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.aleph0_le : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c ↔ ∀ (n : ℕ), ↑n ≤ c
-- Mathlib.RingTheory.Valuation.Basic
Valuation.comap_supp : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {S : Type u_7} [inst_2 : CommRing S] (f : S →+* R), (Valuation.comap f v).supp = Ideal.comap f v.supp
-- Mathlib.Order.Interval.Set.SurjOn
surjOn_Ioo_of_monotone_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Surjective f → ∀ (a b : α), Set.SurjOn f (Set.Ioo a b) (Set.Ioo (f a) (f b))
-- Init.Data.String.Slice
String.Slice.instInhabitedSplitIterator : {a : String.Slice → Type} →
  {a_1 : Type} →
    {a_2 : a_1} →
      {a_3 : String.Slice} →
        {a_4 : String.Slice.Pattern.ToForwardSearcher a_2 a} → Inhabited (String.Slice.SplitIterator a_2 a_3)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_C_mul : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R} {x : R},
  Polynomial.eval x (Polynomial.C a * p) = a * Polynomial.eval x p
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDeriv.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (f : E → F) (x v : E),
  lineDeriv 𝕜 f x v = deriv (fun t => f (x + t • v)) 0
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_obj_obj : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) (y : D),
  ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction C D).obj x).obj y =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x y
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A category `HasEqualizers` if it has all limits of shape `WalkingParallelPair`, i.e. if it has
an equalizer for every parallel pair of morphisms.  -/
CategoryTheory.Limits.HasEqualizers : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SavedState.mk.injEq : ∀ («meta» : Lean.Meta.SavedState) (grind : Lean.Meta.Grind.State) (meta_1 : Lean.Meta.SavedState)
  (grind_1 : Lean.Meta.Grind.State),
  ({ «meta» := «meta», grind := grind } = { «meta» := meta_1, grind := grind_1 }) = («meta» = meta_1 ∧ grind = grind_1)
-- Init.Omega.IntList
/-- Like `List.set`, but right-pad with zeroes as necessary first.  -/
Lean.Omega.IntList.set : Lean.Omega.IntList → ℕ → ℤ → Lean.Omega.IntList
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.proper : {s : String.Slice} →
  (needle : String.Slice) →
    (table : Vector ℕ needle.utf8ByteSize) →
      table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle →
        String.Pos.Raw →
          (needlePos : String.Pos.Raw) → needlePos < needle.rawEndPos → String.Slice.Pattern.ForwardSliceSearcher s
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandler.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (key : Lean.Name) (kind : Lean.Elab.ConfigEval.EvalConfigItemHandlerKind) (body : Lean.Term)
  (projFn? struct? : Option Lean.Name),
  sizeOf { ref := ref, key := key, kind := kind, body := body, projFn? := projFn?, struct? := struct? } =
    1 + sizeOf ref + sizeOf key + sizeOf kind + sizeOf body + sizeOf projFn? + sizeOf struct?
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.inv_hom_apply : ∀ {M N : SemiNormedGrp} (e : M ≅ N) (r : M.carrier),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) r) = r
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with
at most as many pigeons as the floor of the average number of pigeons across all pigeonholes.  -/
Finset.exists_card_fiber_lt_of_card_lt_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
  [inst_1 : CommSemiring M] [inst_2 : LinearOrder M] [IsStrictOrderedRing M],
  ↑s.card < t.card • b → ∃ y ∈ t, ↑{x ∈ s | f x = y}.card < b
-- Init.Grind.Norm
Lean.Grind.not_true : (¬True) = False
-- Batteries.Data.List.Interleave
List.left_sublist_interleave : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist (l₁.interleave l₂)
-- Mathlib.Topology.Category.TopPair
/-- The map between the second spaces  -/
TopPair.Hom.snd : {X Y : TopPair} → (X ⟶ Y) → (TopPair.snd ⟶ TopPair.snd)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instTopologicalSpace : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    {E : ι → Type u_3} →
      {F : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : (i : ι) → TopologicalSpace (E i)] →
            [inst_2 : (i : ι) → AddCommGroup (E i)] →
              [inst_3 : (i : ι) → Module 𝕜 (E i)] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [IsTopologicalAddGroup F] → TopologicalSpace (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_sub_nat_mul_pi : ∀ (x : ℝ) (n : ℕ), Real.tan (x - ↑n * Real.pi) = Real.tan x
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} (hom hom_1 : S₁.apex ⟶ S₂.apex) (e_hom : hom = hom_1)
  (hom_l : CategoryTheory.CategoryStruct.comp hom S₂.l = S₁.l)
  (hom_r : CategoryTheory.CategoryStruct.comp hom S₂.r = S₁.r),
  { hom := hom, hom_l := hom_l, hom_r := hom_r } = { hom := hom_1, hom_l := ⋯, hom_r := ⋯ }
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- The linear equivalence between the fractional ideal `I` and the integral ideal `I.num`
defined by mapping `x` to `I.den • x`, assuming scalar multiplication by `I.den` is injective.  -/
FractionalIdeal.equivNumOfIsSMulRegular : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            [FaithfulSMul R P] → {I : FractionalIdeal S P} → IsSMulRegular P I.den → ↥↑I ≃ₗ[R] ↥I.num
-- Init.Data.Nat.Gcd
Nat.gcd_assoc : ∀ (m n k : ℕ), (m.gcd n).gcd k = m.gcd (n.gcd k)
-- Mathlib.Topology.UniformSpace.Closeds
singleton_mem_hausdorffEntourage : ∀ {α : Type u_1} (U : SetRel α α) (x y : α), ({x}, {y}) ∈ hausdorffEntourage U ↔ (x, y) ∈ U
-- Mathlib.Algebra.Polynomial.Div
Polynomial.div_modByMonic_unique : ∀ {R : Type u} [inst : Ring R] {f g : Polynomial R} (q r : Polynomial R),
  g.Monic → r + g * q = f ∧ r.degree < g.degree → f /ₘ g = q ∧ f %ₘ g = r
-- Mathlib.Algebra.Homology.Double
/-- Let `c : ComplexShape ι`, and `i₀` and `i₁` be distinct indices such
that `hi₀₁ : c.Rel i₀ i₁`, then for any `X : C`, the functor which sends
`K : HomologicalComplex C c` to `X ⟶ K.X i` is corepresentable by `double (𝟙 X) hi₀₁`.  -/
HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {ι : Type u_2} →
          {c : ComplexShape ι} →
            {i₀ i₁ : ι} →
              (hi₀₁ : c.Rel i₀ i₁) →
                i₀ ≠ i₁ →
                  (X : C) →
                    ((HomologicalComplex.eval C c i₀).comp
                          (CategoryTheory.coyoneda.obj (Opposite.op X))).CorepresentableBy
                      (HomologicalComplex.double (CategoryTheory.CategoryStruct.id X) hi₀₁)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.termZ : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.norm_expSeries_div_summable : ∀ {𝔸 : Type u_1} [inst : NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] (x : 𝔸), Summable fun n => ‖x ^ n / ↑n.factorial‖
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- An auxiliary definition for `liftHomotopyZero`.  -/
CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {P : CategoryTheory.ProjectiveResolution Y} →
          {Q : CategoryTheory.ProjectiveResolution Z} →
            (f : P.complex ⟶ Q.complex) → CategoryTheory.CategoryStruct.comp f Q.π = 0 → (P.complex.X 1 ⟶ Q.complex.X 2)
-- Mathlib.Tactic.Simps.Basic
/-- is this a projection that is changed by the user?  -/
Simps.ParsedProjectionData.isCustom : Simps.ParsedProjectionData → Bool
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.isTightMeasureSet_of_tendsto_measure_norm_gt : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : NormedAddCommGroup E]
  [ProperSpace E],
  Filter.Tendsto (fun r => ⨆ μ ∈ S, μ {x | r < ‖x‖}) Filter.atTop (nhds 0) → MeasureTheory.IsTightMeasureSet S
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_of_liftProp : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'}
  {s : Set M},
  (∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) →
    ChartedSpace.LiftProp P g → ChartedSpace.LiftPropOn P g s
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_mul_left_right_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime x (y + x * z) ↔ IsCoprime x y
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.π_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {W : C} (k : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f k = 0) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f k h) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.mk : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {α : Type v} →
        [inst : PartialOrder α] →
          (rank : ↑P.II → α) → (∀ {x y : ↑P.II}, P.AncestralRel x y → rank x < rank y) → P.RankFunction α
-- Init.GrindInstances.ToInt
Lean.Grind.instModUSizeUintNumBits : Lean.Grind.ToInt.Mod USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.top_mul' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (b : WithTop α), ⊤ * b = if b = 0 then 0 else ⊤
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instSMul : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {N : Type u_6} →
                  [inst_4 : TopologicalSpace N] →
                    [inst_5 : ChartedSpace H N] →
                      {n : WithTop ℕ∞} →
                        {V : Type u_10} →
                          [inst_6 : NormedAddCommGroup V] →
                            [inst_7 : NormedSpace 𝕜 V] → SMul 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
-- Init.Data.UInt.Bitwise
UInt8.toUInt32_shiftLeft_of_lt : ∀ (a b : UInt8), b < 8 → (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32 % 256