mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Reflection
/-- This rather technical-looking lemma exists because it is exactly what is needed to establish a
uniqueness result for root data. See the doc string of `Module.Dual.eq_of_preReflection_mapsTo` for
further remarks.  -/
Module.Dual.eq_of_preReflection_mapsTo' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [CharZero R]
  [IsDomain R] [Module.IsTorsionFree R M] {x : M} {Φ : Set M},
  Φ.Finite →
    x ∈ Submodule.span R Φ →
      ∀ {f g : Module.Dual R M},
        f x = 2 →
          Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ →
            g x = 2 →
              Set.MapsTo (⇑(Module.preReflection x g)) Φ Φ →
                (Submodule.span R Φ).subtype.dualMap f = (Submodule.span R Φ).subtype.dualMap g
-- Lean.Elab.App
/-- (quick filter) Return true if `type` contains a binder `[C ...]` where `C` is a class containing outparams.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.isNextOutParamOfLocalInstanceAndResult.hasLocalInstanceWithOutParams : Lean.Environment → Lean.Expr → Bool
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.isRefl_dynEntourage : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} [U.IsRefl], (Dynamics.dynEntourage T U n).IsRefl
-- Init.Data.Nat.Lemmas
Nat.pow_self_mul_pow_self_le : ∀ {m n : ℕ}, m ^ m * n ^ n ≤ (m + n) ^ (m + n)
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.decidableBlockTriangular : {α : Type u_1} →
  {m : Type u_3} →
    {R : Type v} →
      {M : Matrix m m R} →
        {b : m → α} →
          [inst : LT α] →
            [inst_1 : Zero R] → [DecidableEq R] → [Fintype m] → [DecidableLT α] → Decidable (M.BlockTriangular b)
-- Mathlib.Algebra.Group.Graph
MonoidHom.mem_mgraph : ∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] [inst_1 : Monoid H] {f : G →* H} {x : G × H},
  x ∈ f.mgraph ↔ f x.1 = x.2
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.instOfIsFractionRing : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsFractionRing R S],
  Algebra.QuasiFinite R S
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring is closed under addition.  -/
Subsemiring.add_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {x y : R}, x ∈ s → y ∈ s → x + y ∈ s
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_tensor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
  F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
        (CategoryTheory.Functor.LaxMonoidal.μ F Y Y'))
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.isColimit_mk : ∀ {C : Type u} {F : C → Type v} (c : CategoryTheory.Limits.CofanTypes F),
  (∀ (x : c.pt), ∃ i y, c.inj i y = x) →
    (∀ (i : C), Function.Injective (c.inj i)) →
      (∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j) → CategoryTheory.Functor.CoconeTypes.IsColimit c
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.0.CategoryTheory.Limits.mapPair.match_1.eq_1 : ∀ (motive : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair → Sort u_1)
  (h_1 : Unit → motive { as := CategoryTheory.Limits.WalkingPair.left })
  (h_2 : Unit → motive { as := CategoryTheory.Limits.WalkingPair.right }),
  (match { as := CategoryTheory.Limits.WalkingPair.left } with
    | { as := CategoryTheory.Limits.WalkingPair.left } => h_1 ()
    | { as := CategoryTheory.Limits.WalkingPair.right } => h_2 ()) =
    h_1 ()
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- A `WeierstrassCurve` is in normal form of characteristic = 2 and j = 0, if its `a₁, a₂ = 0`.
In other words it is `Y² + a₃Y = X³ + a₄X + a₆`.  -/
WeierstrassCurve.IsCharTwoJEqZeroNF : {R : Type u_1} → [CommRing R] → WeierstrassCurve R → Prop
-- Mathlib.Data.Seq.Computation
Computation.terminates_of_mem : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s → s.Terminates
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.funUnique_symm_apply : ∀ (ι : Type u_4) (α : Type u_5) [inst : Unique ι] [inst_1 : UniformSpace α],
  ⇑(UniformEquiv.funUnique ι α).symm = uniqueElim
-- Mathlib.Data.Finset.Insert
/-- Useful in proofs by induction.  -/
Finset.forall_of_forall_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} {p : α → Prop} {h : a ∉ s}, (∀ x ∈ Finset.cons a s h, p x) → ∀ x ∈ s, p x
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRiiSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRiiSlice._auto_1) →
    Std.Rii.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RiiSlice α)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
hausdorffMeasure_of_dimH_lt : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X} {d : NNReal},
  dimH s < ↑d → (MeasureTheory.Measure.hausdorffMeasure ↑d) s = 0
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.toIsCompatibleWithShift : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.HasShift C ℤ}
  {inst_2 : CategoryTheory.Preadditive C} {inst_3 : CategoryTheory.Limits.HasZeroObject C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {W : CategoryTheory.MorphismProperty C} [self : W.IsCompatibleWithTriangulation], W.IsCompatibleWithShift ℤ
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- A `2`-transitive action is primitive.  -/
MulAction.isPreprimitive_of_is_two_pretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsMultiplyPretransitive G α 2 → MulAction.IsPreprimitive G α
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- The fixator of a subset of cardinal `d` in an `n`-primitive action
acts `n-d`-primitively on the remaining (`d ≤ n`).  -/
MulAction.ofFixingSubgroup.isMultiplyPreprimitive : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {m n : ℕ}
  [MulAction.IsMultiplyPreprimitive M α n] {s : Set α} [Finite ↑s],
  s.ncard + m = n → MulAction.IsMultiplyPreprimitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
-- Lean.Elab.Term.TermElabM
/-- Create a new metavariable with the given type, and try to synthesize it.
If type class resolution cannot be executed (e.g., it is stuck because of metavariables in `type`),
register metavariable as a pending one.
 -/
Lean.Elab.Term.mkInstMVar : Lean.Expr → optParam (Option Lean.MessageData) none → Lean.Elab.TermElabM Lean.Expr
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.valuesIter.eq_1 : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.HashMap α β), m.valuesIter = m.inner.valuesIter
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.append_const_left : ∀ {w3 w1 a w2 b : ℕ} {c : BitVec w3},
  BitVec.ofNat w1 a ++ (BitVec.ofNat w2 b ++ c) = BitVec.cast ⋯ (BitVec.ofNat w1 a ++ BitVec.ofNat w2 b ++ c)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.mul_comm : ∀ {R : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A]
  [IsScalarTower R A A] [SMulCommClass R A A] (a b : A), quasispectrum R (a * b) = quasispectrum R (b * a)
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.applyAssignment.go : Array Lean.Expr → ℕ → ℕ → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Unit
-- Aesop.Tree.Data
_private.Aesop.Tree.Data.0.Bool.toYesNo : Bool → Std.Format
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.insertIfNew₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, h⟩ a b)).WF
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- A collection of sets of E-matching theorems.  -/
Lean.Meta.Grind.EMatchTheoremsArray : Type
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.isImmersion_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsImmersion f ↔ AlgebraicGeometry.IsPreimmersion f ∧ IsLocallyClosed (Set.range ⇑f)
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
/-- Restriction of scalars for a crystallographic root pairing.  -/
RootPairing.restrictScalars : {ι : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Field L] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : Module L M] →
                [inst_4 : Module L N] →
                  (P : RootPairing ι L M N) →
                    (K : Type u_5) →
                      [inst_5 : Field K] →
                        [inst_6 : Algebra K L] →
                          [inst_7 : Module K M] →
                            [inst_8 : Module K N] →
                              [IsScalarTower K L M] →
                                [IsScalarTower K L N] →
                                  [P.IsBalanced] →
                                    [P.IsCrystallographic] →
                                      RootPairing ι K ↥(Submodule.span K (Set.range ⇑P.root))
                                        ↥(Submodule.span K (Set.range ⇑P.coroot))
-- Init.Data.String.Basic
String.Slice.Pos.cast_startPos : ∀ {s t : String.Slice} {hst : s.copy = t.copy}, s.startPos.cast hst = t.startPos
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
/-- A bicategory structure on pseudofunctors, with strong transformations as 1-morphisms.

Note that this instance is scoped to the `Pseudofunctor.StrongTrans` namespace.  -/
CategoryTheory.Pseudofunctor.StrongTrans.instBicategory : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    (C : Type u₂) →
      [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.Bicategory (CategoryTheory.Pseudofunctor B C)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.instGroup : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Group (Matrix.SpecialLinearGroup n R)
-- Init.Data.List.Basic
List.length_append : ∀ {α : Type u} {as bs : List α}, (as ++ bs).length = as.length + bs.length
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (toContinuousMap : C(α, β)) (zero_at_infty' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (nhds 0))
  (toContinuousMap_1 : C(α, β))
  (zero_at_infty'_1 : Filter.Tendsto toContinuousMap_1.toFun (Filter.cocompact α) (nhds 0)),
  ({ toContinuousMap := toContinuousMap, zero_at_infty' := zero_at_infty' } =
      { toContinuousMap := toContinuousMap_1, zero_at_infty' := zero_at_infty'_1 }) =
    (toContinuousMap = toContinuousMap_1)
-- Mathlib.Data.Finset.Image
Equiv.finsetCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (e' : β ≃ γ),
  e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side.  -/
EuclideanGeometry.dist_div_tan_oangle_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₃ p₁).tan = dist p₃ p₂
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
/-- An oracle that uses the Simplex Algorithm.  -/
Mathlib.Tactic.Linarith.CertificateOracle.simplexAlgorithmSparse : Mathlib.Tactic.Linarith.CertificateOracle
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_prod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct G H],
  CategoryTheory.IsCoseparator (G ⨯ H) ↔ (CategoryTheory.ObjectProperty.pair G H).IsCoseparating
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffOn.cle_arrowCongr : ∀ {𝕜 : 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_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_11}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {f : M → F₁ ≃L[𝕜] F₂}
  {g : M → F₃ ≃L[𝕜] F₄} {s : Set M},
  ContMDiffOn I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n (fun x => ↑(f x).symm) s →
    ContMDiffOn I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) n (fun x => ↑(g x)) s →
      ContMDiffOn I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) n (fun y => ↑((f y).arrowCongr (g y))) s
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.hasSum_integral_of_summable_integral_norm : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_4} [Countable ι] {F : ι → α → E},
  (∀ (i : ι), MeasureTheory.Integrable (F i) μ) →
    (Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ) → HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
-- Mathlib.Tactic.Linarith.Parsing
/-- Linear combinations of monomials are represented by mapping monomials to coefficients.  -/
Mathlib.Tactic.Linarith.Sum : Type
-- Mathlib.Algebra.GCDMonoid.Basic
Irreducible.gcd_eq_one_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {x y : α},
  Irreducible x → (gcd x y = 1 ↔ ¬x ∣ y)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.finsuppProd_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] (f : ι →₀ N) (m : ι → N → M) (r : ι → N → R),
  (f.prod fun i n => AddMonoidAlgebra.single (m i n) (r i n)) = AddMonoidAlgebra.single (f.sum m) (f.prod r)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_takeEndWhile_eq_true : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String}, s.endsWith pat = false → (s.takeEndWhile pat).isEmpty = true
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter₂_vsub_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VSub α β] (s : (i : ι) → κ i → Set β)
  (t : Set β), (⋂ i, ⋂ j, s i j) -ᵥ t ⊆ ⋂ i, ⋂ j, s i j -ᵥ t
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom_toPshHom : ∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.Scheme) (f : X ⟶ Y.toPresheafedSpace)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f).toPshHom = f
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.stronglyMeasurable_cauchyPDFReal : ∀ (x₀ : ℝ) (γ : NNReal), MeasureTheory.StronglyMeasurable (ProbabilityTheory.cauchyPDFReal x₀ γ)
-- Mathlib.Algebra.Order.Interval.Basic
instOneNonemptyInterval.eq_1 : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], instOneNonemptyInterval = { one := NonemptyInterval.pure 1 }
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_sup_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U₁ U₂ V : Submodule 𝕜 E}, U₁ ⊔ U₂ ⟂ V ↔ U₁ ⟂ V ∧ U₂ ⟂ V
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- The SNF relation between the vectors of the bases.  -/
Module.Basis.SmithNormalForm.snf : ∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  {ι : Type u_4} {n : ℕ} (self : Module.Basis.SmithNormalForm N ι n) (i : Fin n),
  ↑(self.bN i) = self.a i • self.bM (self.f i)
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- The underlying `BialgHom`.  -/
HopfAlgCat.Hom.toBialgHom' : {R : Type u} → [inst : CommRing R] → {V W : HopfAlgCat R} → V.Hom W → V.carrier →ₐc[R] W.carrier
-- Init.Data.Nat.Gcd
Nat.gcd_def : ∀ (x y : ℕ), x.gcd y = if x = 0 then y else (y % x).gcd x
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Adding an analytic function to a meromorphic one does not change the pole divisor.  -/
MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E},
  AnalyticOnNhd 𝕜 f₁ U → MeromorphicOn f₂ U → (MeromorphicOn.divisor (f₁ + f₂) U)⁻ = (MeromorphicOn.divisor f₂ U)⁻
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_injective : ∀ {M : Type u_2} [inst : Mul M], Function.Injective Subsemigroup.unop
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- The Dirichlet density of the empty set is `0`.  -/
NumberField.Set.dirichletDensity_empty : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], NumberField.Set.dirichletDensity ∅ = 0
-- Lean.Data.PersistentArray
Lean.mkPArray : {α : Type u} → ℕ → α → Lean.PArray α
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.exposeLevelMVars : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.row_weak : ∀ {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → T i j1 ≤ T i j2
-- Mathlib.Algebra.Module.PointwisePi
vadd_pi_subset : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → VAdd K (R i)] (r : K) (s : Set ι)
  (t : (i : ι) → Set (R i)), r +ᵥ s.pi t ⊆ s.pi (r +ᵥ t)
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The lower topology on a partial order is T₀.  -/
Topology.IsLower.t0Space : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α], T0Space α
-- Init.Data.SInt.Lemmas
Int16.toInt16_toISize : ∀ (n : Int16), n.toISize.toInt16 = n
-- Mathlib.Topology.Defs.Induced
Topology.isOpenEmbedding_iff : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y),
  Topology.IsOpenEmbedding f ↔ Topology.IsEmbedding f ∧ IsOpen (Set.range f)
-- Mathlib.Data.ZMod.Basic
/-- `val a` is a natural number defined as:
- for `a : ZMod 0` it is the absolute value of `a`
- for `a : ZMod n` with `0 < n` it is the least natural number in the equivalence class

See `ZMod.valMinAbs` for a variant that takes values in the integers.
 -/
ZMod.val : {n : ℕ} → ZMod n → ℕ
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.map_sub : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} (R' : Type u_11) [inst_2 : Ring R']
  [inst_3 : MulSemiringAction M R'] (S' : Type u_13) [inst_4 : Ring S'] [inst_5 : MulSemiringAction N S']
  (f : R' →ₑ+*[φ] S') (x y : R'), f (x - y) = f x - f y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.congr_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ → (t₁.Equiv t₃ ↔ t₂.Equiv t₃)
-- Mathlib.Algebra.Group.Submonoid.Support
/-- **Alias** of `Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem`. -/
Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem₂ : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, M.IsMulPointed → ∀ {x : G}, x ∈ M → x⁻¹ ∈ M → x = 1
-- Mathlib.Data.Nat.Nth
Nat.nth_strictMonoOn : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite), StrictMonoOn (Nat.nth p) (Set.Iio hf.toFinset.card)
-- Mathlib.Topology.NatEmbedding
/-- In an infinite Hausdorff topological space, there exists a sequence of pairwise disjoint
infinite open sets.  -/
exists_seq_infinite_isOpen_pairwise_disjoint : ∀ (X : Type u_1) [inst : TopologicalSpace X] [T2Space X] [Infinite X],
  ∃ U, (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen (U n)) ∧ Pairwise (Function.onFun Disjoint U)
-- Init.Data.String.Substring
/-- Returns the longest common prefix of two substrings.

The returned substring uses the same underlying string as `s`.
 -/
Substring.Raw.commonPrefix : Substring.Raw → Substring.Raw → Substring.Raw
-- Std.Internal.Do.Order.Basic
/-- Indexed infimum  -/
Lean.Order.«term⨅_,_» : Lean.ParserDescr
-- Mathlib.RingTheory.Localization.Basic
instIsLocalizationAlgebraMapSubmonoid : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (Rₘ : Type u_4) [inst_1 : CommSemiring Rₘ]
  [inst_2 : Algebra R Rₘ] [IsLocalization M Rₘ], IsLocalization (Algebra.algebraMapSubmonoid R M) Rₘ
-- Init.Data.Array.Count
Array.count_push : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {xs : Array α},
  Array.count a (xs.push b) = Array.count a xs + if (b == a) = true then 1 else 0
-- Mathlib.Tactic.Translate.Core
/-- Verify that the type of `srcDecl` translates to that of `tgtDecl`.
Also try to autogenerate the `reorder` and `relevant_arg` options for this translation.  -/
Mathlib.Tactic.Translate.checkExistingType : Mathlib.Tactic.Translate.TranslateData →
  Lean.Name →
    Lean.Name →
      Mathlib.Tactic.Translate.Config →
        optParam Bool true → Lean.MetaM (Mathlib.Tactic.Translate.Reorder × Mathlib.Tactic.Translate.RelevantArg)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited γ] {f : α → β → Option γ}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValue! k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
        ((Std.Internal.List.getValue? k l).pbind fun v h => f (Std.Internal.List.getKey k l ⋯) v).get!
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.erase_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, ∅.erase k = ∅
-- Lean.Meta.Basic
/-- Collect forward dependencies for the free variables in `toRevert`.
Recall that when reverting free variables `xs`, we must also revert their forward dependencies.

When `generalizeNondepLet := true` (the default), then the values of nondependent lets are not considered
when computing forward dependencies.
 -/
Lean.Meta.collectForwardDeps : Array Lean.Expr → Bool → optParam Bool true → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `reallyPersist` converts an array of pairs `(fvar, mvar)` to another array of the same type.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.reallyPersist : Array (Lean.FVarId × Lean.MVarId) →
  List Lean.MVarId → List Lean.MVarId → Lean.MetavarContext → Lean.MetavarContext → Array (Lean.FVarId × Lean.MVarId)