mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) (X_1 : Cᵒᵖ)
  (a :
    (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).comp
              (CategoryTheory.sheafToPresheaf J (Type (max v w)))).obj
          X).obj
      X_1),
  (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaCompSheafToPresheaf.inv.app X).app X_1)) a = a
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mk_le_mk : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S S' : AddSubmonoid M}
  (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier)
  (h' : ∀ (c : R) {x : M}, x ∈ S'.carrier → c • x ∈ S'.carrier),
  { toAddSubmonoid := S, smul_mem' := h } ≤ { toAddSubmonoid := S', smul_mem' := h' } ↔ S ≤ S'
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.mk.injEq : ∀ {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 : S₁.apex ⟶ S₂.apex)
  (hom_l : autoParam (CategoryTheory.CategoryStruct.comp hom S₂.l = S₁.l) CategoryTheory.Span.Hom.hom_l._autoParam)
  (hom_r : autoParam (CategoryTheory.CategoryStruct.comp hom S₂.r = S₁.r) CategoryTheory.Span.Hom.hom_r._autoParam)
  (hom_1 : S₁.apex ⟶ S₂.apex)
  (hom_l_1 : autoParam (CategoryTheory.CategoryStruct.comp hom_1 S₂.l = S₁.l) CategoryTheory.Span.Hom.hom_l._autoParam)
  (hom_r_1 : autoParam (CategoryTheory.CategoryStruct.comp hom_1 S₂.r = S₁.r) CategoryTheory.Span.Hom.hom_r._autoParam),
  ({ hom := hom, hom_l := hom_l, hom_r := hom_r } = { hom := hom_1, hom_l := hom_l_1, hom_r := hom_r_1 }) =
    (hom = hom_1)
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
/-- **Alias** of the reverse direction of `MeasureTheory.memLp_pi_iff`. -/
MeasureTheory.MemLp.of_eval : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p : ENNReal} {ι : Type u_2} [inst : Fintype ι]
  {E : ι → Type u_3} [inst_1 : (i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i},
  (∀ (i : ι), MeasureTheory.MemLp (fun x => f x i) p μ) → MeasureTheory.MemLp f p μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.tendsto_abs_tan_atTop : ∀ (k : ℤ),
  Filter.Tendsto (fun x => |Real.tan x|) (nhdsWithin ((2 * ↑k + 1) * Real.pi / 2) {(2 * ↑k + 1) * Real.pi / 2}ᶜ)
    Filter.atTop
-- Lean.DocString.Add
/-- Adds a Markdown docstring to the environment, validating documentation links.
 -/
Lean.addMarkdownDocString : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT IO m] →
      [Lean.MonadOptions m] →
        [Lean.MonadEnv m] →
          [Lean.MonadError m] →
            [Lean.MonadLog m] →
              [Lean.AddMessageContext m] → Lean.Name → Lean.TSyntax `Lean.Parser.Command.docComment → m Unit
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.map_under : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (J : Ideal S), Ideal.map (algebraMap R S) (Ideal.under R J) = J
-- Mathlib.Topology.Algebra.InfiniteSum.Group
summable_neg_iff : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f : β → α}, Summable (fun b => -f b) L ↔ Summable f L
-- Init.Tactics
/-- `mrename_i` is like `rename_i`, but names inaccessible stateful hypotheses in a `Std.Do.SPred` goal.
 -/
Lean.Parser.Tactic.mrenameIMacro : Lean.ParserDescr
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.essFiniteType_cond_iff : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (σ : Finset S),
  IsLocalization (Submonoid.comap (algebraMap (↥(Algebra.adjoin R ↑σ)) S) (IsUnit.submonoid S)) S ↔
    ∀ (s : S), ∃ t ∈ Algebra.adjoin R ↑σ, IsUnit t ∧ s * t ∈ Algebra.adjoin R ↑σ
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.of_relative_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {P : CategoryTheory.MorphismProperty C} {a b : C} {f : a ⟶ b},
  CategoryTheory.MorphismProperty.relative F P (F.map f) → P f
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The change-of-basis matrix between two orthonormal bases `a`, `b` is a unitary matrix.  -/
OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (a b : OrthonormalBasis ι 𝕜 E),
  a.toBasis.toMatrix ⇑b ∈ Matrix.unitaryGroup ι 𝕜
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkLinebreakBefore.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.instRing : {R : Type u} → [inst : CommRing R] → (self : BialgCat R) → Ring self.carrier
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.map_normal : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal],
  (AddSubgroup.map (QuotientAddGroup.mk' N) M).Normal
-- Lean.Meta.Hint
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.splitChars : String → Array Char
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a homomorphism `φ : G →* H`
with a right inverse `ψ : H → G`.  -/
QuotientGroup.quotientKerEquivOfRightInverse : {G : Type u} →
  [inst : Group G] →
    {H : Type v} → [inst_1 : Group H] → (φ : G →* H) → (ψ : H → G) → Function.RightInverse ψ ⇑φ → G ⧸ φ.ker ≃* H
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.isPrincipal_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (S : Submodule R M), S.IsPrincipal ↔ ∃ a, S = R ∙ a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.Y_sub_Y_mul_Y_sub_negY : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q →
      P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → (P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) * (P 1 * Q 2 ^ 3 - W'.negY Q * P 2 ^ 3) = 0
-- Mathlib.Data.Int.Bitwise
Int.ldiff.eq_2 : ∀ (m n : ℕ), (Int.ofNat m).ldiff (Int.negSucc n) = ↑(m &&& n)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The braiding isomorphism can be passed through a map by swapping the order.  -/
CategoryTheory.Limits.braid_natural_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z_1 : C} (h : W ⨯ Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding Y W).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g f) h)
-- Init.Data.SInt.Basic
instModInt16 : Mod Int16
-- Mathlib.Order.Basic
le_of_forall_lt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ c < a, c < b) → a ≤ b
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.d₁₂_apply_apply_ofTrivial : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsTrivial L M] (f : LieModule.Cohomology.oneCochain R L M) (x y : L),
  (((LieModule.Cohomology.d₁₂ R L M) f) x) y = -f ⁅x, y⁆
-- Mathlib.Topology.UniformSpace.Cauchy
CompleteSpace.snd_of_prod : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] [CompleteSpace (α × β)]
  [h : Nonempty α], CompleteSpace β
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanImportKind : Lean.ToJson Lean.Lsp.LeanImportKind
-- Mathlib.Data.PFun
PFun.mem_fix_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β},
  b ∈ f.fix a ↔ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
-- Lean.Parser.Term
Lean.Parser.Term.app : Lean.Parser.TrailingParser
-- Init.Data.Int.Lemmas
Int.negSucc_ne_zero : ∀ (n : ℕ), Int.negSucc n ≠ 0
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Multiset.Nat.antidiagonalTuple_zero_zero : Multiset.Nat.antidiagonalTuple 0 0 = {![]}
-- Mathlib.Topology.Compactness.Compact
Set.Finite.isCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s.Finite → IsCompact s
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
/-- **Alias** of `SkewMonoidAlgebra.coeff_erase_apply`. -/
SkewMonoidAlgebra.erase_apply_toFinsupp : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α),
  ((SkewMonoidAlgebra.erase a) f).coeff = Finsupp.erase a f.coeff
-- Lean.Environment
Lean.OLeanEntries.exported : {α : Type} → Lean.OLeanEntries α → α
-- Mathlib.Analysis.Analytic.Basic
AnalyticOnNhd.analyticOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  AnalyticOnNhd 𝕜 f s → AnalyticOn 𝕜 f s
-- Mathlib.GroupTheory.Exponent
Subgroup.pow_exponent_eq_one : ∀ {G : Type u} [inst : Group G] {H : Subgroup G} {g : G}, g ∈ H → g ^ Monoid.exponent ↥H = 1
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_mul : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {V : Finset α},
  ↑((SzemerediRegularity.star hP G ε hU V).biUnion id).card ≤
    ↑(SzemerediRegularity.star hP G ε hU V).card * (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1)
-- Mathlib.Algebra.Ring.Defs
Ring.toIntCast : {R : Type u} → [self : Ring R] → IntCast R
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.prop_shift_iff_of_isStableUnderShift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {G : Type u_4}
  [inst_1 : AddGroup G] [inst_2 : CategoryTheory.HasShift C G] [P.IsStableUnderShift G] [P.IsClosedUnderIsomorphisms]
  (X : C) (g : G), P ((CategoryTheory.shiftFunctor C g).obj X) ↔ P X
-- Mathlib.NumberTheory.NumberField.AdeleRing
/-- `AdeleRing (𝓞 K) K` is the adele ring of a number field `K`.

More generally `AdeleRing R K` can be used if `K` is the field of fractions
of the Dedekind domain `R`. This enables use of rings like `AdeleRing ℤ ℚ`, which
in practice are easier to work with than `AdeleRing (𝓞 ℚ) ℚ`.

Note that this definition does not give the correct answer in the function field case.
 -/
NumberField.AdeleRing : (R : Type u_1) →
  (K : Type u_2) →
    [inst : CommRing R] →
      [IsDedekindDomain R] → [inst_2 : Field K] → [inst_3 : Algebra R K] → [IsFractionRing R K] → Type (max u_2 u_2 u_1)
-- Mathlib.Logic.Basic
eq_comm_eq : ∀ {α : Sort u_1} (a b : α), (a = b) = (b = a)
-- Lean.Meta.Tactic.NormCast
/-- elim lemma: LHS has 0 head coes and ≥ 1 internal coe  -/
Lean.Meta.NormCast.Label.elim : Lean.Meta.NormCast.Label
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [inst_1 : Ring R] (v : Valuation R Γ)
  [hv : v.IsRankOneDiscrete] (a : WithZero ↥(MonoidWithZeroHom.ofClass v).valueGroup),
  (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v) a =
    (WithZero.map' ↑(intEquivOfZPowersEqTop (Valuation.IsRankOneDiscrete.generator' v)⁻¹ ⋯).symm) a
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.List.map_unattach.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} → (motive : Subtype P → Sort u_2) → (x : Subtype P) → ((x : α) → (h : P x) → motive ⟨x, h⟩) → motive x
-- Lean.Parser.Term
Lean.Parser.Term.posConfigItem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Option.Basic
Option.iget_of_mem : ∀ {α : Type u_1} [inst : Inhabited α] {a : α} {o : Option α}, a ∈ o → o.iget = a
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.of_subsingleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X] [Subsingleton X] (f : X → Y),
  Topology.IsInducing f
-- Mathlib.Analysis.Calculus.Deriv.Abs
contDiffWithinAt_abs : ∀ {n : ℕ∞} {x : ℝ}, x ≠ 0 → ∀ (s : Set ℝ), ContDiffWithinAt ℝ (↑n) (fun x => |x|) s x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (f : c ⟶ c'),
  H.mapConeMorphism f = (CategoryTheory.Limits.Cone.functoriality F H).map f
-- Mathlib.Topology.Compactness.Compact
instNoncompactSpaceInt : NoncompactSpace ℤ
-- Mathlib.Order.Basic
exists_ge_of_linear : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), ∃ c, a ≤ c ∧ b ≤ c
-- Mathlib.Order.TypeTags
/-- Recursor for `WithTop` using the preferred forms `⊤` and `↑a`.  -/
WithTop.recTopCoe : {α : Type u_1} → {C : WithTop α → Sort u_2} → C ⊤ → ((a : α) → C ↑a) → (n : WithTop α) → C n
-- Init.Data.String.Modify
/-- Replaces each character in `s` with the result of applying `Char.toUpper` to it.

`Char.toUpper` has no effect on characters outside of the range `'a'`–`'z'`.

Examples:
* `"orange".toUpper = "ORANGE"`
* `"abc123".toUpper = "ABC123"`
 -/
String.toUpper : String → String
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The map into the completion is uniform-inducing.  -/
AbstractCompletion.isUniformInducing : ∀ {α : Type u} [inst : UniformSpace α] (self : AbstractCompletion.{v, u} α), IsUniformInducing self.coe
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.Eqv.of_zero_scalar : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (f : (i : ι) → s i), PiTensorProduct.Eqv R s (FreeAddMonoid.of (0, f)) 0
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- We use `Num` to define the translation of binary natural numbers. Positive numbers are
translated using `trPosNum`, and `trNum 0 = []`. So there are never any trailing `bit0`'s in
a translated `Num`.

```
    0 = []
    1 = [bit1]
    2 = [bit0, bit1]
    3 = [bit1, bit1]
    4 = [bit0, bit0, bit1]
```
 -/
Turing.PartrecToTM2.trNum : Num → List Turing.PartrecToTM2.Γ'
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.lTensor_zero : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U}, Representation.IntertwiningMap.lTensor ρ 0 = 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instInhabited : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → Inhabited (SchwartzMap E F)
-- Mathlib.Topology.ContinuousMap.Polynomial
polynomialFunctions_separatesPoints : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (X : Set R),
  (polynomialFunctions X).SeparatesPoints
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.instNonempty : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [Nonempty M] {S : L.ElementarySubstructure M},
  Nonempty ↥S
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_xor_distrib_left : ∀ {a b c : ℕ}, a &&& (b ^^^ c) = a &&& b ^^^ a &&& c
-- Mathlib.CategoryTheory.Sites.Sieves
/-- the factorisation of the morphism  -/
CategoryTheory.Presieve.FunctorPushforwardStructure.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} {S : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X}
  (self : CategoryTheory.Presieve.FunctorPushforwardStructure F S f),
  f = CategoryTheory.CategoryStruct.comp self.lift (F.map self.premap)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_self_inter`. -/
Set.diff_self_inter : ∀ {α : Type u_1} {s t : Set α}, s \ (s ∩ t) = s \ t
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginSeriesTerm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x y : E),
  (((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y) = (p (k + l)) (s.piecewise (fun x_1 => x) fun x => y)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.isMonHom_fst_id_right : ∀ {M S : AlgebraicGeometry.Scheme} [inst : M.Over S] [inst_1 : CategoryTheory.MonObj (M.asOver S)],
  CategoryTheory.IsMonHom
    (AlgebraicGeometry.Scheme.Hom.asOver
      (CategoryTheory.Limits.pullback.fst (M ↘ S) (CategoryTheory.CategoryStruct.id S)) S)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_single_zero_mul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ},
  ((HahnSeries.single 0) r * x).coeff a = r * x.coeff a
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.linearIndependent_pair_iff_ne : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {D D' : Projectivization K V}, LinearIndependent K ![D.rep, D'.rep] ↔ D ≠ D'
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.even_nat_card_aut_of_not_isUnramified : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  ¬NumberField.InfinitePlace.IsUnramified k w → Even (Nat.card Gal(K/k))
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.adj_injective : ∀ {V : Type u_2}, Function.Injective Digraph.Adj
-- Mathlib.Topology.MetricSpace.Thickening
IsClopen.of_cthickening_subset_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {δ : ℝ}, 0 < δ → Metric.cthickening δ s ⊆ s → IsClopen s
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- An empty type is a charted space over any topological space.  -/
ChartedSpace.empty : (H : Type u_5) →
  [inst : TopologicalSpace H] → (M : Type u_6) → [inst_1 : TopologicalSpace M] → [IsEmpty M] → ChartedSpace H M
-- Mathlib.Order.Ideal
Order.Ideal.biSup_finset_mem_iff : ∀ {P : Type u_1} [inst : CompleteLattice P] {I : Order.Ideal P} {α : Type u_2} {f : α → P} {s : Finset α},
  ⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp U.toSpecΓ hU.fromSpec = U.ι
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- If `X` has a right dual in a braided category, then it has a left dual.  -/
CategoryTheory.BraidedCategory.hasLeftDualOfHasRightDual : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → {X : C} → [CategoryTheory.HasRightDual X] → CategoryTheory.HasLeftDual X
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.hy : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (self : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  g self.y = self.s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v' : β k')
  (l r : Std.DTreeMap.Internal.Impl α β) (hlk_2 : k ∈ Std.DTreeMap.Internal.Impl.inner size k' v' l r),
  (Std.DTreeMap.Internal.Impl.inner size k' v' l r).getEntry k hlk_2 =
    match h : compare k k' with
    | Ordering.lt => l.getEntry k ⋯
    | Ordering.gt => r.getEntry k ⋯
    | Ordering.eq => ⟨k', v'⟩
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Bound.0.termM : Lean.ParserDescr
-- Mathlib.Data.NNReal.Basic
NNReal.toReal_finsuppSum : ∀ {M : Type u_1} [inst : Zero M] {ι : Type u_2} (f : ι →₀ M) (g : ι → M → NNReal),
  ↑(f.sum g) = f.sum fun i m => ↑(g i m)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_laxMonoidalToAddMon_obj_add : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add (CategoryTheory.CategoryStruct.id F.X)
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableSup₂.measurable_sup : ∀ {M : Type u_1} {inst : MeasurableSpace M} {inst_1 : Max M} [self : MeasurableSup₂ M], Measurable fun p => p.1 ⊔ p.2
-- Plausible.Tactic
/-- `plausible` considers a proof goal and tries to generate examples
that would contradict the statement.

Let's consider the following proof goal.

```lean
xs : List Nat,
h : ∃ (x : Nat) (H : x ∈ xs), x < 3
⊢ ∀ (y : Nat), y ∈ xs → y < 5
```

The local constants will be reverted and an instance will be found for
`Testable (∀ (xs : List Nat), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5))`.
The `Testable` instance is supported by an instance of `Sampleable (List Nat)`,
`Decidable (x < 3)` and `Decidable (y < 5)`.

Examples will be created in ascending order of size (more or less)

The first counter-examples found will be printed and will result in an error:

```
===================
Found problems!
xs := [1, 28]
x := 1
y := 28
-------------------
```

If `plausible` successfully tests 100 examples, it acts like
admit. If it gives up or finds a counter-example, it reports an error.

For more information on writing your own `Sampleable` and `Testable`
instances, see `Testing.Plausible.Testable`.

Optional arguments given with `plausible (config := { ... })`
* `numInst` (default 100): number of examples to test properties with
* `maxSize` (default 100): final size argument

Options:
* `set_option trace.plausible.decoration true`: print the proposition with quantifier annotations
* `set_option trace.plausible.discarded true`: print the examples discarded because they do not
  satisfy assumptions
* `set_option trace.plausible.shrink.steps true`: trace the shrinking of counter-example
* `set_option trace.plausible.shrink.candidates true`: print the lists of candidates considered
  when shrinking each variable
* `set_option trace.plausible.instance true`: print the instances of `testable` being used to test
  the proposition
* `set_option trace.plausible.success true`: print the tested samples that satisfy a property
 -/
plausibleSyntax : Lean.ParserDescr
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.get_bind_set : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m],
  (do
      let s ← get
      set s) =
    pure PUnit.unit
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Use `edge_getElem_darts` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.getElem_edges_eq_edge_getElem_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (h : i < p.edges.length),
  p.edges[i] = p.darts[i].edge
-- Lean.Meta.WHNF
Lean.Meta.reduceBoolNative : Lean.Name → Lean.MetaM Bool