mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varFinset.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (i : α), (FirstOrder.Language.var i).varFinset = {i}
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_indep_iff_exists' : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M✶.Indep I ↔ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.nsmul_period_add_vadd : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] (n : ℕ) (m : M) (a : α),
  (AddAction.period m a + n) • m +ᵥ a = n • m +ᵥ a
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_iExsUnique : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {γ : Type u_3} [inst_1 : Finite γ]
  {φ : L.Formula (α ⊕ γ)} {v : α → M} {v' : Fin 0 → M},
  FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.Formula.iExsUnique γ φ) v v' ↔
    ∃! i, φ.Realize (Sum.elim v i)
-- Mathlib.Algebra.Group.Action.Basic
MulAction.bijective : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (g : α), Function.Bijective fun x => g • x
-- Mathlib.Analysis.Convex.Combination
/-- The centroid can be regarded as a center of mass.  -/
Finset.centroid_eq_centerMass : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι),
  s.Nonempty → ∀ (p : ι → E), Finset.centroid R s p = s.centerMass (Finset.centroidWeights R s) p
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_blockDiagonal' : ∀ {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] [inst_2 : Zero R] [inst_3 : DecidableEq l] {A : X → (i : l) → Matrix (m' i) (n' i) R},
  Continuous A → Continuous fun x => Matrix.blockDiagonal' (A x)
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_le_contentIdeal_of_dvd : ∀ {R : Type u_3} [inst : CommSemiring R] {p q : Polynomial R}, p ∣ q → q.contentIdeal ≤ p.contentIdeal
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instInhabited : (R : Type u) → [inst : CommRing R] → Inhabited (AlgCat R)
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxcHasSize.eq_1 : Int64.instRxcHasSize = { size := fun lo hi => (hi.toInt + 1 - lo.toInt).toNat }
-- Mathlib.Algebra.Opposites
AddOpposite.op_comp_unop : ∀ {α : Type u_1}, AddOpposite.op ∘ AddOpposite.unop = id
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_X_mul : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {p : Polynomial R},
  p ≠ 0 → (Polynomial.X * p).natDegree = p.natDegree + 1
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_eq_zero_of_not_exists_basis : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (¬∃ s, Nonempty (Module.Basis (↥s) R S)) → Algebra.trace R S = 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedPurity.default : Lean.Compiler.LCNF.Purity
-- Std.Http.Data.Chunk
/-- A validated chunk extension value that ensures all characters conform to HTTP standards per RFC 9112 §7.1.1.
Extension values appear in chunked transfer encoding as metadata associated with extension names.

Note: UTF-8 encoding is not supported. The quoting mechanism is strict and only permits escaping
specific values. Additionally, the library does not support obs-text, which means certain UTF-8
characters or values outside of token, qdtext, and the limited set of escapable characters cannot be
encoded.

Reference: https://httpwg.org/specs/rfc9112.html#chunked.extension
 -/
Std.Http.Chunk.ExtensionValue : Type
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic completion of `K` is a normed field.  -/
NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsDedekindDomain R] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                [Module.Finite ℤ R] →
                  [Module.Free ℤ R] → NormedField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.diag_map_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct (X ⨯ Y) (X ⨯ Y)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X ⨯ Y))
      (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) =
    CategoryTheory.CategoryStruct.id (X ⨯ Y)
-- Mathlib.Computability.Partrec
Nat.rfindOpt_mono : ∀ {α : Type u_1} {f : ℕ → Option α},
  (∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n) → ∀ {a : α}, a ∈ Nat.rfindOpt f ↔ ∃ n, a ∈ f n
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_eq_one' : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M},
  s.mulIndicator f = 1 ↔ Disjoint (Function.mulSupport f) s
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.instProductivenessRelation : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        [inst_1 : Std.IteratorAccess α m] →
          [inst_2 : Monad m] →
            [Std.Iterators.Productive α m] →
              Std.Iterators.ProductivenessRelation (Std.Iterators.Types.StepSizeIterator α m β) m
-- Lean.Expr
/-- A set of unique free variable identifiers.
This is a persistent data structure implemented using `Std.TreeSet`.  -/
Lean.FVarIdSet : Type
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The inclusion of a summand in a tensor product of two graded objects.  -/
CategoryTheory.GradedObject.Monoidal.ιTensorObj : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (X₁ X₂ : CategoryTheory.GradedObject I C) →
            [inst_3 : X₁.HasTensor X₂] →
              (i₁ i₂ i₁₂ : I) →
                i₁ + i₂ = i₁₂ →
                  (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶
                    CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ i₁₂)
-- Mathlib.CategoryTheory.Action.Basic
/-- The category of actions of `G` in the category `V`
is equivalent to the functor category `SingleObj G ⥤ V`.
 -/
Action.functorCategoryEquivalence : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) → [inst_1 : Monoid G] → Action V G ≌ CategoryTheory.Functor (CategoryTheory.SingleObj G) V
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.isLocallyFiniteMeasure_of_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {_m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
  [H : MeasureTheory.IsLocallyFiniteMeasure μ], ν ≤ μ → MeasureTheory.IsLocallyFiniteMeasure ν
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.disjoint_corootSpan_ker_corootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [IsDomain R] [inst_5 : Module R M] [inst_6 : Module R N]
  (P : RootPairing ι R M N) [P.IsAnisotropic], Disjoint (P.corootSpan R) (LinearMap.ker P.CorootForm)
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
/-- The distinguished triangle in the derived category associated to a short
exact sequence of cochain complexes.  -/
DerivedCategory.triangleOfSES : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} →
          S.ShortExact → CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Postcomposing `f` with `Prod.fst` is `C^n` at `(x, y)`  -/
ContDiffAt.fst : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F × G} {x : E},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (fun x => (f x).1) x
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.applySimpResultToLocalDeclCore : Lean.MVarId → Lean.FVarId → Option (Lean.Expr × Lean.Expr) → Lean.MetaM (Option (Lean.FVarId × Lean.MVarId))
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The composition operator (in the target) with a Lipschitz map is uniformly continuous.  -/
BoundedContinuousFunction.uniformContinuous_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G),
  UniformContinuous (BoundedContinuousFunction.comp G H)
-- Mathlib.Algebra.Algebra.Pi
/-- `R`-algebra homomorphism between the function spaces `ι → A` and `ι → B`, induced by an
`R`-algebra homomorphism `f` between `A` and `B`.  -/
AlgHom.compLeft : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → (ι : Type u_4) → (ι → A) →ₐ[R] ι → B
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.baseChange_polynomialX : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange B).polynomialX = (MvPolynomial.map ↑f) (W'.baseChange A).polynomialX
-- Mathlib.Algebra.BigOperators.Finprod
/-- This version does not assume that `ι` is finite (compare `Nat.cast_finprod`), but instead needs
to assume characteristic zero to deal with the infinite case.  -/
Nat.cast_finprod' : ∀ {ι : Type u_3} {R : Type u_7} [inst : CommSemiring R] [CharZero R] (f : ι → ℕ),
  ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)
-- Mathlib.Order.Lattice
sup_eq_sup_iff_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b
-- Mathlib.Topology.Sets.Compacts
/-- The converting map from relatively compact opens
neighbourhood of a compact subset to its opens neighbourhoods  -/
TopologicalSpace.Compacts.openRcNhdsToOpenNhds : {α : Type u_1} → [inst : TopologicalSpace α] → (K : TopologicalSpace.Compacts α) → ↑K.openRcNhds → ↑K.openNhds
-- Init.Data.Nat.Div.Basic
Nat.mod.eq_2 : ∀ (x n : ℕ), n.succ.mod x = if x ≤ n.succ then n.succ.modCore x else n.succ
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set β},
  MeasurableSet s → (κ.fst a) s = (κ a) {p | p.1 ∈ s}
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.NatTrans.pi'_app : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {E : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} E] {F G : CategoryTheory.Functor E ((i : I) → C i)}
  (τ : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ⟶ G.comp (CategoryTheory.Pi.eval C i)) (X : E) (i : I),
  (CategoryTheory.NatTrans.pi' τ).app X i = (τ i).app X
-- Mathlib.Topology.Sets.Compacts
/-- A homeomorphism induces an equivalence on compact sets, by taking the image.  -/
TopologicalSpace.Compacts.equiv : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → α ≃ₜ β → TopologicalSpace.Compacts α ≃ TopologicalSpace.Compacts β
-- Lean.Meta.Sym.Pattern
/-- Structural definitional equality for applications with `ProofInstInfo`.
Skips proof arguments (proof irrelevance) and defers instance arguments to `isDefEqI`.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqAppWithInfo : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Sym.ProofInstInfo → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.RingTheory.RingHomProperties
/-- A property of ring homomorphisms `P` is said to have finite products, if a finite product of
algebras satisfying `Q` also satisfies `P`.  -/
RingHom.HasFiniteProducts : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- A class of objects which have a right dual.  -/
CategoryTheory.HasRightDual : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → Type (max u₁ v₁)
-- Lean.Meta.Tactic.Grind.Util
Lean.Meta.Grind.isDIte : Lean.Expr → Bool
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, k ∈ Std.HashMap.map f m → k ∈ m
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_below_le`. -/
Ideal.inertiaDeg'_below_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.IsPrime] [r.LiesOver q] [Module.Finite R T], q.inertiaDeg R ≤ r.inertiaDeg R
-- Mathlib.Analysis.Analytic.Order
AnalyticOnNhd.analyticOrderAt_eq_top_iff_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [PreconnectedSpace 𝕜] {f : 𝕜 → E} (z : 𝕜),
  (∀ (z₀ : 𝕜), AnalyticAt 𝕜 f z₀) → (analyticOrderAt f z = ⊤ ↔ f = 0)
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lieAlgebra : {R : Type u} →
  {ι : Type v} →
    [inst : CommRing R] →
      (L : ι → Type w) →
        [inst_1 : (i : ι) → LieRing (L i)] → [(i : ι) → LieAlgebra R (L i)] → LieAlgebra R (DirectSum ι fun i => L i)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
liouville_liouvilleNumber : ∀ {m : ℕ}, 2 ≤ m → Liouville (liouvilleNumber ↑m)
-- Std.Http.Data.Method
/-- Merge a version-controlled resource.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-11.2
 -/
Std.Http.Method.merge : Std.Http.Method
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The glued scheme (`(gluing 𝒰 f g).glued`) is indeed the pullback of `f` and `g`.  -/
AlgebraicGeometry.Scheme.Pullback.gluedIsLimit : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          CategoryTheory.Limits.IsLimit
            (CategoryTheory.Limits.PullbackCone.mk (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g)
              (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) ⋯)
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.optionT : Lean.Elab.Do.MonadInfo →
  Lean.Name →
    Lean.Name →
      Lean.Elab.Do.DoElabM (Lean.Elab.Do.DoElabM Lean.Expr) → Lean.Elab.Do.ControlStack → Lean.Elab.Do.ControlStack
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomEquiv_comp_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : V} (h : (X ⟶[V] Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.eHomEquiv V) f)
          ((CategoryTheory.eHomEquiv V) g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h))
-- Std.Data.Iterators.Producers.Repeat
_private.Std.Data.Iterators.Producers.Repeat.0.Std.Iterators.Types.RepeatIterator.instProductivenessRelation : {α : Type w} → {f : α → α} → Std.Iterators.ProductivenessRelation (Std.Iterators.Types.RepeatIterator α f) Id
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuous_lift_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  {hf : ∀ (x y : X), Inseparable x y → f x = f y}, Continuous (SeparationQuotient.lift f hf) ↔ Continuous f
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- A cone is limit iff it is so after the application of `coyoneda.obj X` for all `X : Cᵒᵖ`.  -/
CategoryTheory.Limits.Cone.isLimitCoyonedaEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone F) →
            CategoryTheory.Limits.IsLimit c ≃
              ((X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((CategoryTheory.coyoneda.obj X).mapCone c))
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toLinearMap_inj : ∀ {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₁ e₂ : M ≃ₛₗ[σ] M₂},
  ↑e₁ = ↑e₂ ↔ e₁ = e₂
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.instFinite : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M], Module.Finite R M
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.orderIsoRpow_symm_apply : ∀ (y : ℝ) (hy : 0 < y), (ENNReal.orderIsoRpow y hy).symm = ENNReal.orderIsoRpow (1 / y) ⋯
-- Mathlib.Topology.LocallyClosed
coborder_eq_union_frontier_compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, coborder s = s ∪ (frontier s)ᶜ
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.map_restrictAppIso_hom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U) {Z : Ab}
  (h : M.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((M.restrict f).presheaf.map hUV)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M V).hom
      (CategoryTheory.CategoryStruct.comp (M.presheaf.map (CategoryTheory.homOfLE ⋯).op) h)
-- Init.Data.Vector.Basic
Vector.Mem.mk : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {a : α}, a ∈ xs.toArray → xs.Mem a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_lt_pi_div_two : ∀ (x : ℝ), Real.arctan x < Real.pi / 2
-- Init.Tactics
/-- `apply_assumption` looks for an assumption of the form `... → ∀ _, ... → head`
where `head` matches the current goal.

You can specify additional rules to apply using `apply_assumption [...]`.
By default `apply_assumption` will also try `rfl`, `trivial`, `congrFun`, and `congrArg`.
If you don't want these, or don't want to use all hypotheses, use `apply_assumption only [...]`.
You can use `apply_assumption [-h]` to omit a local hypothesis.
You can use `apply_assumption using [a₁, ...]` to use all lemmas which have been labelled
with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).

`apply_assumption` will use consequences of local hypotheses obtained via `symm`.

If `apply_assumption` fails, it will call `exfalso` and try again.
Thus if there is an assumption of the form `P → ¬ Q`, the new tactic state
will have two goals, `P` and `Q`.

You can pass a further configuration via the syntax `apply_rules (config := {...}) lemmas`.
The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
 -/
Lean.Parser.Tactic.applyAssumption : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- The `Finset` of length-`n` walks from `u` to `v`.
This is used to give `{p : G.walk u v | p.length = n}` a `Fintype` instance, and it
can also be useful as a recursive description of this set when `V` is finite.

See `SimpleGraph.coe_finsetWalkLength_eq` for the relationship between this `Finset` and
the set of length-`n` walks.  -/
SimpleGraph.finsetWalkLength : {V : Type u} → (G : SimpleGraph V) → [DecidableEq V] → [G.LocallyFinite] → ℕ → (u v : V) → Finset (G.Walk u v)
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.InfiniteAdeleRing.norm_def : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.InfiniteAdeleRing K),
  ‖x‖ = ∏ v, ‖x v‖ ^ v.mult
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The full subcategory of fibrant objects.  -/
HomotopicalAlgebra.FibrantObject : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithFibrations C] → [CategoryTheory.Limits.HasTerminal C] → Type u
-- Init.Data.List.Sublist
List.IsPrefix.head : ∀ {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <+: l₂) (hx : l₁ ≠ []), l₁.head hx = l₂.head ⋯
-- Mathlib.Topology.MetricSpace.Bounded
/-- The distance between two points in a set is controlled by the diameter of the set.  -/
Metric.dist_le_diam_of_mem' : ∀ {α : Type u} {s : Set α} {x y : α} [inst : PseudoMetricSpace α],
  Metric.ediam s ≠ ⊤ → x ∈ s → y ∈ s → dist x y ≤ Metric.diam s
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define a `StrongNormalizedGCDMonoid` structure on a monoid just from
the existence of a `lcm`.  -/
strongNormalizedGCDMonoidOfExistsLCM : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [StrongNormalizationMonoid α] →
        [DecidableEq α] → (∀ (a b : α), ∃ c, ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d) → StrongNormalizedGCDMonoid α
-- Init.Data.Rat.Basic
Rat.instLE : LE ℚ
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.inclusion_range : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h_le : H ≤ K), (Subgroup.inclusion h_le).range = H.subgroupOf K
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.preorder : {d : ℕ} → Preorder (ℤ√↑d)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.div_opow_log_lt : ∀ {b : Ordinal.{u_1}} (o : Ordinal.{u_1}), 1 < b → o / b ^ Ordinal.log b o < b
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Coercion of a trivialization to a function. We don't use `e.toFun` in the `CoeFun` instance
because it is actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about
`toPartialEquiv`. While we may want to switch to this behavior later, doing it mid-port will break a
lot of proofs.  -/
Bundle.Trivialization.toFun' : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} → [inst_2 : TopologicalSpace Z] → Bundle.Trivialization F proj → Z → B × F
-- Lean.Expr
Lean.MVarIdSet.insert : Lean.MVarIdSet → Lean.MVarId → Lean.MVarIdSet
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.natAddLEFunctor_obj_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n k l : ℕ} (h : k + l ≤ n) {R : CategoryTheory.ComposableArrows C n},
  R.Exact → ((CategoryTheory.ComposableArrows.natAddLEFunctor h).obj R).Exact
-- Mathlib.NumberTheory.EulerProduct.ExpLog
/-- A variant of the Euler Product formula in terms of the exponential of a sum of logarithms.  -/
EulerProduct.exp_tsum_primes_log_eq_tsum : ∀ {f : ℕ →*₀ ℂ},
  (Summable fun x => ‖f x‖) → Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - f ↑p)) = ∑' (n : ℕ), f n