mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.Language
Language.reverseIso_apply : ∀ (α : Type u_1) (l : Language α), (Language.reverseIso α) l = MulOpposite.op l.reverse
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.mk : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α},
  (∀ (aig : Std.Sat.AIG α) (input : β aig), aig.decls.size ≤ (f aig input).aig.decls.size) →
    (∀ (aig : Std.Sat.AIG α) (input : β aig) (idx : ℕ) (h1 : idx < aig.decls.size)
        (h2 : idx < (f aig input).aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]) →
      Std.Sat.AIG.LawfulOperator α β f
-- Lean.Meta.Match.MatchEqsExt
/-- Returns `true` if `declName` is the name of a `match` equational theorem.
 -/
Lean.Meta.Match.isMatchEqnTheorem : Lean.Environment → Lean.Name → Bool
-- Mathlib.NumberTheory.NumberField.CMField
/-- A field `K` is `CM` if `K` is a totally complex quadratic extension of its maximal
real subfield `K⁺`.
 -/
NumberField.IsCMField : (K : Type u_1) → [inst : Field K] → [CharZero K] → Prop
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_eq_getD_back?_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.maxD fallback = t.toArray.back?.getD fallback
-- Mathlib.Analysis.SumIntegralExpDecay
intervalIntegral_pow_mul_exp_neg_le : ∀ {k : ℕ} {M c : ℝ}, 0 ≤ M → 0 < c → ∫ (x : ℝ) in 0..M, x ^ k * Real.exp (-(c * x)) ≤ ↑k.factorial / c ^ (k + 1)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.trunc_C_mul_T : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ) (r : R),
  LaurentPolynomial.trunc (LaurentPolynomial.C r * LaurentPolynomial.T n) =
    if 0 ≤ n then (Polynomial.monomial n.toNat) r else 0
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.instPatternModel : {pat : String} → String.Slice.Pattern.Model.PatternModel pat
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite products of analytic functions are analytic  -/
Finset.analyticWithinAt_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A}
  {c : E} {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (∏ n ∈ N, f n) s c
-- Mathlib.Order.RelIso.Basic
/-- A function `f : α → β` induces a relation homomorphism from an `α`-relation `r` to
`Relation.Map r f f`.  -/
RelHom.toMap : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (f : α → β) → r →r Relation.Map r f f
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_toAffineMap : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (f : P →ᴬ[R] Q), ⇑↑f = ⇑f
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.IsTruncLE.mem_prev : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} [self : e.IsTruncLE]
  {i' : ι'} {j : ι}, c'.Rel i' (e.f j) → ∃ i, e.f i = i'
-- Mathlib.Data.Set.Basic
Set.powerset_inter : ∀ {α : Type u} (s t : Set α), 𝒫 (s ∩ t) = 𝒫 s ∩ 𝒫 t
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of `ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem₀`. -/
ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_notMem₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∏ j ∈ s, f j) (f i) μ
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
/-- For quadratic forms on finite-dimensional spaces, the maximal finrank of a negative-definite
subspace of `M`. (Defined as `0` if `M` is infinite-dimensional).  -/
sigNeg : {R : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommGroup M] → [inst_1 : CommRing R] → [LinearOrder R] → [inst_3 : Module R M] → QuadraticForm R M → ℕ
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.isPlausibleStep_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] {it : Std.Iter α}
  {step : Std.IterStep (Std.Iter α) α}, it.IsPlausibleStep step ↔ step = Std.Rxc.Iterator.step it
-- Lean.DocString.Parser
/-- The context within which a newline element is parsed.
 -/
Lean.Doc.Parser.InlineCtxt : Type
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `contMDiffOn_baseSet_localFrameCoeff`.

---

If `s` is `C^k` on `e.baseSet`, so is its coefficient `b.localFrameCoeff e i`
in the local frame induced by `e`  -/
contMDiffOn_baseSet_localFrame_coeff : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {k : WithTop ℕ∞}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) e.baseSet →
    ∀ (i : ι),
      ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) k ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s)
        e.baseSet
-- Mathlib.Tactic.Translate.Core
/-- Run `applyReplacementFun` on an expression `fun x₁ .. xₙ ↦ e`,
making sure not to translate type-classes on `xᵢ` if `i` is in `dontTranslate`.  -/
Mathlib.Tactic.Translate.applyReplacementLambda : Mathlib.Tactic.Translate.TranslateData →
  List ℕ → Lean.Expr → Lean.MetaM (Lean.Expr × Option Mathlib.Tactic.Translate.RelevantArg)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.coe_toEquiv : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b),
  ⇑e.toEquiv = ⇑e
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.add_apply : ∀ {R : Type} [inst : Ring R] {M N : CategoryTheory.Mat R} (f g : M ⟶ N) (i : M.obj) (j : N.obj),
  (f + g) i j = f i j + g i j
-- Batteries.Data.Vector.Lemmas
Vector.getElem_scanr_zero : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  (Vector.scanr f init as)[0] = Vector.foldr f init as
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.restrict_toMeasurable_of_cover : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {v : ℕ → Set α},
  s ⊆ ⋃ n, v n → (∀ (n : ℕ), μ (s ∩ v n) ≠ ⊤) → μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- The natural transformation `F ⟶ H` that exists for every adjoint triple `F ⊣ G ⊣ H` where `F`
and `H` are fully faithful, given here as the whiskered unit `F ⟶ F ⋙ G ⋙ H` of the second
adjunction followed by the inverse of the whiskered unit `F ⋙ G ⋙ H ⟶ H` of the first.  -/
CategoryTheory.Adjunction.Triple.leftToRight : {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] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {H : CategoryTheory.Functor C D} → CategoryTheory.Adjunction.Triple F G H → [F.Full] → [F.Faithful] → F ⟶ H
-- Lean.Parser.Basic
Lean.Parser.dbgTraceState : String → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- A number satisfies the Liouville condition with any exponent if and only if it is a Liouville
number.  -/
forall_liouvilleWith_iff : ∀ {x : ℝ}, (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x
-- Lean.Data.NameTrie
/-- Returns the value of the longest key in `t` that is a prefix of `k`, if any.  -/
Lean.NameTrie.findLongestPrefix? : {β : Type u_1} → Lean.NameTrie β → Lean.Name → Option β
-- Mathlib.Order.Sublocale
Sublocale.restrict_of_mem : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} {a : X} (ha : a ∈ S), S.restrict a = ⟨a, ha⟩
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C)
  [inst_3 : CategoryTheory.Limits.HasMultiequalizer I]
  [inst_4 : CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer I)) (i : J.L),
  ↑((CategoryTheory.Limits.Concrete.multiequalizerEquiv I) x) i =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι I i)) x
-- Mathlib.CategoryTheory.Category.Pairwise
/-- An equivalence between the "proxy type" `CategoryTheory.Pairwise.proxyType` and `CategoryTheory.Pairwise`. The proxy type is a reducible definition that represents the inductive type using `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum` (and whatever other inductive types appear within the inductive type), and the intended use is to define typeclass instances uses pre-existing instances on these. (Generated by the `proxy_equiv%` elaborator.) -/
CategoryTheory.Pairwise.proxyTypeEquiv : (ι : Type v) → ι ⊕ (_ : ι) × ι ≃ CategoryTheory.Pairwise ι
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.mk.sizeOf_spec : ∀ (p : Lean.Grind.Linarith.Poly) (h : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof),
  sizeOf { p := p, h := h } = 1 + sizeOf p + sizeOf h
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentSelector : Type
-- Mathlib.Algebra.Algebra.StrictPositivity
IsStrictlyPositive.isSelfAdjoint : ∀ {A : Type u_1} [inst : Semiring A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A] {a : A},
  IsStrictlyPositive a → IsSelfAdjoint a
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.entries : Lean.Meta.SimpAll.State → Array Lean.Meta.SimpAll.Entry
-- Mathlib.Algebra.MvPolynomial.Equiv
_private.Mathlib.Algebra.MvPolynomial.Equiv.0.Option.elim.match_1.splitter : {α : Type u_1} →
  {β : Sort u_3} →
    (motive : Option α → β → (α → β) → Sort u_2) →
      (x : Option α) →
        (x_1 : β) →
          (x_2 : α → β) →
            ((x : α) → (x_3 : β) → (f : α → β) → motive (some x) x_3 f) →
              ((y : β) → (x : α → β) → motive none y x) → motive x x_1 x_2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_erase!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase! k t).getKey? k = none
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddMonCat.adjoinZero_map : ∀ {X Y : AddSemigrp} (f : X ⟶ Y),
  AddMonCat.adjoinZero.map f = AddMonCat.ofHom (WithZero.mapAddHom (AddSemigrp.Hom.hom f))
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_bot : ∀ {α : Type u_2} [inst : TopologicalSpace α], ↑⊥ = ∅
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.subarrayMeasure.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (es : Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))),
  Lean.PersistentHashMap.subarrayMeasure es = (List.map (fun x => x.measure) (Std.Slice.toList es)).sum
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_cons_apply : ∀ {α : Type u} {β : α → Type v} {γ : Type w} {l : Std.DHashMap.Raw α β} {acc : List γ} (f : (a : α) → β a → γ),
  Std.DHashMap.Raw.fold (fun acc k v => f k v :: acc) acc l =
    List.map (fun p => f p.fst p.snd) (Std.DHashMap.Internal.toListModel l.buckets).reverse ++ acc
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.denest_nest : ∀ (p : DyckWord), p.nest.denest ⋯ = p
-- Std.Time.Format
/-- Parses a `String` in the `LongDateFormat` and returns a `PlainDateTime` object in the GMT time zone.
 -/
Std.Time.PlainDateTime.fromLongDateFormatString : String → Except String Std.Time.PlainDateTime
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.ofScientific_mem : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] (s : S) {b : Bool}
  {n m : ℕ}, OfScientific.ofScientific n b m ∈ s
-- Mathlib.CategoryTheory.Yoneda
/-- Unification hint for `(uliftYoneda.obj X).obj (op Y) ≃ ULift (Y ⟶ X)`.  -/
CategoryTheory.uliftYoneda_obj_obj_eq_hom : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → C → C → C → Prop
-- Mathlib.Tactic.Linarith.Preprocessing
/-- If `h` is an equality or inequality between natural numbers,
`natToInt` lifts this inequality to the integers.
It also adds the facts that the integers involved are nonnegative.
To avoid adding the same nonnegativity facts many times, it is a global preprocessor.
 -/
Mathlib.Tactic.Linarith.natToInt : Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.isEquiv_of_lt_one_imp : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Semifield S] [inst_2 : LinearOrder S]
  {v w : AbsoluteValue R S} [IsStrictOrderedRing S] [Archimedean S] [ExistsAddOfLE S],
  v.IsNontrivial → (∀ (x : R), v x < 1 → w x < 1) → v.IsEquiv w
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- This definition endows a completely pseudometrizable space with a complete pseudometric.
Use it as: `letI := upgradeIsCompletelyPseudoMetrizable X`.  -/
TopologicalSpace.upgradeIsCompletelyPseudoMetrizable : (X : Type u_3) →
  [inst : TopologicalSpace X] →
    [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X] →
      TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace X
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.indep_iSup_directed_limsup : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4}
  {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) → ProbabilityTheory.Kernel.Indep (⨆ a, ⨆ n ∈ ns a, s n) (Filter.limsup s f) κ μα
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- We relate a finite product over primes in `s` to an infinite sum over `s`-factored numbers.  -/
EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  f 1 = 1 →
    (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
      (∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖) →
        ∀ (s : Finset ℕ),
          (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set α},
  s.Nonempty → s • Set.univ = Set.univ
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.zero_beq_eq_ite : ∀ {b : Bool} {a : BitVec 1}, ((0#1 == a) == b) = (a == bif b then 0#1 else 1#1)
-- Init.Data.UInt.Lemmas
UInt64.lt_or_eq_of_le : ∀ {a b : UInt64}, a ≤ b → a < b ∨ a = b
-- Init.Data.Order.MinMaxOn
maxOn_self : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : α}, maxOn f x x = x
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.multiplicity_sup : ∀ {R : Type u_3} [inst : CommRing R] [IsDedekindDomain R] (p : IsDedekindDomain.HeightOneSpectrum R) {I J : Ideal R},
  I ≠ ⊥ → J ≠ ⊥ → multiplicity p.asIdeal (I ⊔ J) = min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.instEquivLike.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G},
  AddGroupExtension.Equiv.instEquivLike =
    { coe := fun equiv => ⇑equiv.toAddEquiv, inv := fun equiv => ⇑equiv.symm, left_inv := ⋯, right_inv := ⋯,
      coe_injective' := ⋯ }
-- Init.Data.Fin.Basic
/-- Adds a natural number to a `Fin`, increasing the bound.

This is a generalization of `Fin.succ`.

`Fin.natAdd` is a version of this function that takes its `Nat` parameter first.

Examples:
* `Fin.addNat (5 : Fin 8) 3 = (8 : Fin 11)`
* `Fin.addNat (0 : Fin 8) 1 = (1 : Fin 9)`
* `Fin.addNat (1 : Fin 8) 2 = (3 : Fin 10)`

 -/
Fin.addNat : {n : ℕ} → Fin n → (m : ℕ) → Fin (n + m)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- The embedding of pairs of vectors into the even subalgebra, as a bilinear map.  -/
CliffordAlgebra.even.ι : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (Q : QuadraticForm R M) → CliffordAlgebra.EvenHom Q ↥(CliffordAlgebra.even Q)
-- Mathlib.RingTheory.Coalgebra.Quotient
/-- An `R`-submodule `I` of an `R`-coalgebra `C` is a *coideal* if the counit vanishes on
`I` and the comultiplication descends through the module quotient `C ⧸ I`.  -/
Submodule.IsCoideal : {R : Type u_1} →
  {C : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup C] → [inst_2 : Module R C] → [CoalgebraStruct R C] → Submodule R C → Prop
-- Aesop.Forward.State
/-- Modify the maps for slot `slot` and all later slots.  -/
Aesop.InstMap.modifyMapsForSlotsFrom : Aesop.InstMap →
  Aesop.SlotIndex →
    (Lean.PHashSet Aesop.Match → Lean.PHashSet Aesop.Hyp → Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp) →
      Aesop.InstMap
-- Mathlib.Analysis.Convex.Mul
/-- `x^n`, `n : ℕ` is convex on the whole real line whenever `n` is even.  -/
Even.convexOn_pow : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {n : ℕ},
  Even n → ConvexOn 𝕜 Set.univ fun x => x ^ n
-- Mathlib.Order.Filter.NAry
Filter.map_map₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : Filter α} {g : Filter β} (m : α → β → γ) (n : γ → δ),
  Filter.map n (Filter.map₂ m f g) = Filter.map₂ (fun a b => n (m a b)) f g
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.isComplete_eqLocus : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₂ M₂] {M' : Type u_9}
  [inst_5 : UniformSpace M'] [CompleteSpace M'] [inst_7 : AddCommMonoid M'] [inst_8 : Module R₁ M'] [T2Space M₂]
  (f g : M' →SL[σ₁₂] M₂), IsComplete ↑((↑f).eqLocus ↑g)
-- Std.Time.Date.Unit.Week
Std.Time.Week.instTransOrdOrdinal : Std.TransOrd Std.Time.Week.Ordinal
-- Mathlib.Algebra.Polynomial.Div
Polynomial.divByMonic.eq_1 : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), p /ₘ q = if hq : q.Monic then (p.divModByMonicAux hq).1 else 0
-- Mathlib.LinearAlgebra.Dimension.Torsion.Finite
/-- **Alias** of `Module.rank_eq_zero_iff_isTorsion`. -/
rank_eq_zero_iff_isTorsion : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M],
  Module.rank R M = 0 ↔ Module.IsTorsion R M
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.affine_hasPullback : ∀ {A B C : CommRingCat} (f : AlgebraicGeometry.Spec A ⟶ AlgebraicGeometry.Spec C)
  (g : AlgebraicGeometry.Spec B ⟶ AlgebraicGeometry.Spec C), CategoryTheory.Limits.HasPullback f g
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots_map_le_natDegree : ∀ {A : Type u_3} {B : Type u_4} [inst : Semiring A] [inst_1 : CommRing B] [inst_2 : IsDomain B] {f : A →+* B}
  (p : Polynomial A), (Polynomial.map f p).roots.card ≤ p.natDegree
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U₁ V₁ U₂ V₂ : Submodule 𝕜 E}, U₂ ≤ U₁ → V₂ ≤ V₁ → U₁ ⟂ V₁ → U₂ ⟂ V₂
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β} {h : k' ∈ Std.ExtDHashMap.Const.alter m k f},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.alter m k f) k' h =
    if heq : (k == k') = true then (f (Std.ExtDHashMap.Const.get? m k)).get ⋯ else Std.ExtDHashMap.Const.get m k' ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insertIfNew k v).contains k = true
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.toDeleteEdges_nil : ∀ {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} (hp : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∉ s),
  SimpleGraph.Walk.toDeleteEdges s SimpleGraph.Walk.nil hp = SimpleGraph.Walk.nil
-- Init.Data.Nat.Lcm
Nat.lcm_eq_left : ∀ {m n : ℕ}, n ∣ m → m.lcm n = m
-- Mathlib.RingTheory.RingInvo
/-- The requirement that the ring homomorphism is its own inverse  -/
RingInvo.involution' : ∀ {R : Type u_2} [inst : Semiring R] (self : RingInvo R) (x : R),
  MulOpposite.unop (self.toFun (MulOpposite.unop (self.toFun x))) = x
-- Mathlib.CategoryTheory.Action
CategoryTheory.instCategoryActionCategory : (M : Type u_1) →
  [inst : Monoid M] →
    (X : Type u_2) → [inst_1 : MulAction M X] → CategoryTheory.Category.{u_1, u_2} (CategoryTheory.ActionCategory M X)
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.step : Lean.Name → Array Lean.IR.Decl → Lean.IR.LogEntry
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_3 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (v : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx (Lean.Grind.CommRing.Expr.var v) = ↑(Lean.Grind.CommRing.Var.denote ctx v)
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.length_iterFromIdx : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ}, (xs.iterFromIdx pos).length = n - pos
-- Mathlib.Tactic.TermCongr
/-- `congr(expr)` generates a congruence from an expression containing
congruence holes of the form `$h` or `$(h)`.
In these congruence holes, `h : a = b` indicates that, in the generated congruence,
on the left-hand side `a` is substituted for `$h`
and on the right-hand side `b` is substituted for `$h`.

For example, if `h : a = b` then `congr(1 + $h) : 1 + a = 1 + b`.

This is able to make use of the expected type, for example `(congr(_ + $h) : 1 + _ = _)`
with `h : x = y` gives `1 + x = 1 + y`.
The expected type can be an `Iff`, `Eq`, or `HEq`.
If there is no expected type, then it generates an equality.

Note: the process of generating a congruence lemma involves elaborating the pattern
using terms with attached metadata and a reducible wrapper.
We try to avoid doing so, but these terms can leak into the local context through unification.
This can potentially break tactics that are sensitive to metadata or reducible functions.
Please report anything that goes wrong with `congr(...)` lemmas on Zulip.

For debugging, you can set `set_option trace.Elab.congr true`.
 -/
Mathlib.Tactic.TermCongr.termCongr : Lean.ParserDescr