mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The natural transformation `K.ιTruncLE e : K.truncLE e ⟶ K` for all `K`.  -/
ComplexShape.Embedding.ιTruncLENatTrans : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [inst : e.IsTruncLE] →
            (C : Type u_4) →
              [inst_1 : CategoryTheory.Category.{v_2, u_4} C] →
                [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
                    [inst_4 : CategoryTheory.CategoryWithHomology C] →
                      e.truncLEFunctor C ⟶ CategoryTheory.Functor.id (HomologicalComplex C c')
-- Init.Data.List.Control
/-- Applies the monadic action `f` to every element in the list, in order.

`List.mapM` is a variant that collects results. `List.forA` is a variant that works on any
`Applicative`.
 -/
List.forM : {m : Type u → Type v} → [Monad m] → {α : Type w} → List α → (α → m PUnit.{u + 1}) → m PUnit.{u + 1}
-- Mathlib.CategoryTheory.DinatTrans
/-- Dinatural transformations between two difunctors.  -/
CategoryTheory.DinatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D) →
          CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D) → Type (max u₁ v₂)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.forall_mem_sup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M) {P : M → Prop}, (∀ x ∈ p ⊔ p', P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)
-- Init.Data.String.Lemmas.Pattern.Split.Char
_private.Init.Data.String.Lemmas.Pattern.Split.Char.0.String.Slice.Pattern.Model.split.eq_def : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} (firstRejected curr : s.Pos)
  (hle : firstRejected ≤ curr),
  String.Slice.Pattern.Model.split pat firstRejected curr hle =
    if h : curr = s.endPos then [s.subslice firstRejected curr hle]
    else
      match hd : String.Slice.Pattern.Model.matchAt? pat curr with
      | some pos =>
        have this := ⋯;
        s.subslice firstRejected curr hle :: String.Slice.Pattern.Model.split pat pos pos ⋯
      | none => String.Slice.Pattern.Model.split pat firstRejected (curr.next h) ⋯
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.finiteSpec_map : ∀ (k : Type u) [inst : Field k] {X Y : (CommAlgCat.FiniteEtale k)ᵒᵖ} (f : X ⟶ Y),
  (CommAlgCat.FiniteEtale.finiteSpec k).map f = FintypeCat.homMk (PrimeSpectrum.comap ↑(CommAlgCat.Hom.hom f.unop.hom))
-- Mathlib.FieldTheory.KrullTopology
/-- If `L/K` is an algebraic field extension, then the stabilizer
in `Gal(L/K)` of any element in `L` is open for the Krull topology.  -/
stabilizer_isOpen_of_isIntegral : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsIntegral K L]
  (x : L), IsOpen ↑(MulAction.stabilizer Gal(L/K) x)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeInverse_counitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D),
  (e.changeInverse iso).counitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))
-- Mathlib.NumberTheory.LSeries.ZMod
/-- Explicit formula for `LFunction Φ 0` when `Φ` is even.  -/
ZMod.LFunction_apply_zero_of_even : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ}, Function.Even Φ → ZMod.LFunction Φ 0 = -Φ 0 / 2
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_add : ∀ (x y : ℂ), Complex.cosh (x + y) = Complex.cosh x * Complex.cosh y + Complex.sinh x * Complex.sinh y
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getElem_succ_leftInvSeq_alternatingWord : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i j : B) (p k : ℕ)
  (h : k + 1 < 2 * p),
  (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * p)))[k + 1] =
    (MulAut.conj (cs.simple i)) (cs.leftInvSeq (CoxeterSystem.alternatingWord j i (2 * p)))[k]
-- Init.Data.List.MinMaxIdx
List.minIdxOn_singleton : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {x : α} {f : α → β}, List.minIdxOn f [x] ⋯ = 0
-- Init.Data.Nat.Mod
Nat.mul_lt_mul_left : ∀ {a b c : ℕ}, 0 < a → (a * b < a * c ↔ b < c)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {km fallback : α}, t.minKey? = some km → t.getKeyD km fallback = km
-- Mathlib.Probability.Independence.Conditional
/-- If `f` is a family of mutually conditionally independent random variables
(`iCondIndepFun m' hm' m f μ`) and `S, T` are two disjoint finite index sets, then the tuple formed
by `f i` for `i ∈ S` is conditionally independent of the tuple `(f i)_i` for `i ∈ T`.  -/
ProbabilityTheory.iCondIndepFun.condIndepFun_finset : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {β : ι → Type u_6}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (S T : Finset ι),
  Disjoint S T →
    ProbabilityTheory.iCondIndepFun m' hm' f μ →
      (∀ (i : ι), Measurable (f i)) →
        ProbabilityTheory.CondIndepFun m' hm' (fun a i => f (↑i) a) (fun a i => f (↑i) a) μ
-- Mathlib.Data.Subtype
Subtype.map_injective : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ (a : α), p a → q (f a)),
  Function.Injective f → Function.Injective (Subtype.map f h)
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleFoldingRange.addRanges : Lean.FileMap →
  List (ℕ × Option String.Pos.Raw) → List Lean.Syntax → StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM Unit
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forall_mem_keysArray_iff_forall_mem_getKey : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {p : α → Prop}, m.WF → ((∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h))
-- Mathlib.Analysis.Polynomial.Factorization
/-- If `f : F[X]` is monic of degree `≥ 1` and `F` is an algebraically closed field,
then `f = f₁ * f₂` with `f₁` monic of degree `1` and `f₂` monic of degree `f.natDegree - 1`.  -/
Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_mul_isMonicOfDegree : ∀ {F : Type u_1} [inst : Field F] [IsAlgClosed F] {f : Polynomial F} {n : ℕ},
  f.IsMonicOfDegree (n + 1) → ∃ f₁ f₂, f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a right invariant measure under left addition is right invariant.  -/
MeasureTheory.isMulRightInvariant_map_add_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G}
  [μ.IsAddRightInvariant] (g : G), (MeasureTheory.Measure.map (fun x => g + x) μ).IsAddRightInvariant
-- Lean.Declaration
Lean.instBEqRecursorVal : BEq Lean.RecursorVal
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] {f g : InfTopHom α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.Triangulated.TStructure.instHasInducedTStructurePlus : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C], t.plus.HasInducedTStructure t
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.liftEquivRight_symm_apply : ∀ (R : Type uR) (S : Type uS) (B : Type uB) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (C : Type u_3) [inst_5 : CommRing C] [inst_6 : Algebra R C]
  [inst_7 : Algebra S C] [inst_8 : IsScalarTower R S C] (f : TensorProduct R S B →ₐ[S] C),
  (Algebra.TensorProduct.liftEquivRight R S B C).symm f =
    (AlgHom.restrictScalars R f).comp Algebra.TensorProduct.includeRight
-- Mathlib.NumberTheory.Dioph
Dioph.diophFn_compn : ∀ {α : Type} {n : ℕ} {S : Set (α ⊕ Fin2 n → ℕ)},
  Dioph S → ∀ {f : Vector3 ((α → ℕ) → ℕ) n}, VectorAllP Dioph.DiophFn f → Dioph {v | (Sum.elim v fun i => f i v) ∈ S}
-- Mathlib.Algebra.Order.UpperLower
UpperSet.coe_one : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α], ↑1 = Set.Ici 1
-- Lean.DocString.Types
Lean.Doc.instReprMathMode.repr : Lean.Doc.MathMode → ℕ → Std.Format
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.continuous_rclikeToReal : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜], Continuous ContinuousMap.rclikeToReal
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mkSpanSingleton'_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (x : E) (y : F)
  (H : ∀ (c : R), c • x = 0 → σ c • y = 0) (c : R) (h : c • x ∈ (LinearPMap.mkSpanSingleton' x y H).domain),
  ↑(LinearPMap.mkSpanSingleton' x y H) ⟨c • x, h⟩ = σ c • y
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.Nonneg.eq_1 : ∀ {d : ℕ} (a b : ℤ), { re := a, im := b }.Nonneg = Zsqrtd.Nonnegg d 1 a b
-- Lean.Util.Diff
_private.Lean.Util.Diff.0.Lean.Diff.matchSuffix.go : {α : Type u_1} → [BEq α] → Subarray α → Subarray α → ℕ → Subarray α × Subarray α × Array α
-- Mathlib.Topology.Compactness.CountablyCompact
/-- In a first-countable space, a set is countably compact iff it is sequentially compact.  -/
isCountablyCompact_iff_isSeqCompact : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E} [FirstCountableTopology E],
  IsCountablyCompact A ↔ IsSeqCompact A
-- Mathlib.Algebra.IsPrimePow
instDecidableIsPrimePowNat : {n : ℕ} → Decidable (IsPrimePow n)
-- Mathlib.Data.List.Infix
List.instIsPartialOrderIsInfix : ∀ {α : Type u_1}, IsPartialOrder (List α) fun x1 x2 => x1 <:+: x2
-- Mathlib.RingTheory.Ideal.Over
/-- The set of all prime ideals in `B` that lie over an ideal `p` of `A`.  -/
Ideal.primesOver : {A : Type u_2} →
  [inst : CommSemiring A] → Ideal A → (B : Type u_3) → [inst_1 : Semiring B] → [Algebra A B] → Set (Ideal B)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasProd.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {L : SummationFilter β} [inst : CommMonoid α]
  [inst_1 : TopologicalSpace α] [inst_2 : CommMonoid γ] [inst_3 : TopologicalSpace γ] {f : β → α} {g : β → γ} {a : α}
  {b : γ}, HasProd f a L → HasProd g b L → HasProd (fun x => (f x, g x)) (a, b) L
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.associator.sizeOf_spec : ∀ (e : Lean.Expr) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.StructuralAtom.associator e f g h) =
    1 + sizeOf e + sizeOf f + sizeOf g + sizeOf h
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.eq_homOfEq_iff : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X' = X) (hY : Y' = Y),
  f = Quiver.homOfEq g hX hY ↔ Quiver.homOfEq f ⋯ ⋯ = g
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.add : {α : Type u} → [Mul α] → Add (Additive α)
-- Mathlib.Data.Int.Init
Int.emod_two_eq_zero_or_one : ∀ (n : ℤ), n % 2 = 0 ∨ n % 2 = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialInsert.eq_def : ∀ (a : ℕ) (x : List ℕ),
  SimplexCategoryGenRel.simplicialInsert a x =
    match x with
    | [] => [a]
    | b :: l => if a < b then a :: b :: l else b :: SimplexCategoryGenRel.simplicialInsert (a + 1) l
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.le_iff_adj : ∀ {V : Type u} {G H : SimpleGraph V}, G ≤ H ↔ ∀ (v w : V), G.Adj v w → H.Adj v w
-- Mathlib.Data.Sum.Order
OrderIso.sumLexAssoc_apply_inl_inl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (a : α),
  (OrderIso.sumLexAssoc α β γ) (toLex (Sum.inl (toLex (Sum.inl a)))) = toLex (Sum.inl a)
-- Mathlib.Data.Set.Order
StrictAnti.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  StrictAnti f = ∀ ⦃a b : α⦄, a < b → f b < f a
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.mul : ∀ {F : Type u} {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F] [inst_3 : Algebra K L]
  [inst_4 : Algebra F K] [inst_5 : Algebra F L] [IsScalarTower F K L] (f g : Polynomial F),
  f ≠ 0 →
    g ≠ 0 →
      ∀ [Polynomial.IsSplittingField F K f] [Polynomial.IsSplittingField K L (Polynomial.map (algebraMap F K) g)],
        Polynomial.IsSplittingField F L (f * g)
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.not_ssuperset`.

---

Set notation form of `LE.le.not_gt` -/
HasSubset.Subset.not_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊂ a
-- Mathlib.NumberTheory.Dioph
/-- The sum of squares of a list of polynomials. This is relevant for
Diophantine equations, because it means that a list of equations
can be encoded as a single equation: `x = 0 ∧ y = 0 ∧ z = 0` is
equivalent to `x^2 + y^2 + z^2 = 0`.  -/
Poly.sumsq : {α : Type u_1} → List (Poly α) → Poly α
-- Mathlib.Topology.Bornology.Absorbs
Absorbent.zero_mem : ∀ {G₀ : Type u_1} {E : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [(Bornology.cobounded G₀).NeBot]
  [inst_3 : AddMonoid E] [inst_4 : DistribMulAction G₀ E] {s : Set E}, Absorbent G₀ s → 0 ∈ s
-- Mathlib.Data.Finset.Insert
List.toFinset_eq_empty_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.toFinset = ∅ ↔ l = []
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.eqOn_source : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E],
  Set.EqOn (↑f) (↑f.toContDiffBump ∘ ↑(extChartAt I c)) (chartAt H c).source
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.tendsto_log_nhdsGT_zero : Filter.Tendsto Real.log (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot
-- Lean.Meta.Tactic.Clear
/-- Try to clear the given fvars from the local context.

The fvars must be given in the order they appear in the local context.

See also `tryClearMany'` which takes care of reordering internally,
and returns the cleared hypotheses along with the new goal.
 -/
Lean.MVarId.tryClearMany : Lean.MVarId → Array Lean.FVarId → Lean.MetaM Lean.MVarId
-- Init.Data.Array.Basic
Array.emptyWithCapacity_eq : ∀ {α : Type u_1} {n : ℕ}, Array.emptyWithCapacity n = #[]
-- Mathlib.Topology.Compactification.StoneCech
/-- The extension of a continuous function from `α` to a compact
Hausdorff space `β` to the pre-Stone-Čech compactification of `α`.  -/
preStoneCechExtend : {α : Type u} →
  [inst : TopologicalSpace α] →
    {β : Type v} →
      [inst_1 : TopologicalSpace β] → [T2Space β] → [CompactSpace β] → {g : α → β} → Continuous g → PreStoneCech α → β
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_eq_of_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S}, ↑a₂ + b₁ = ↑b₂ + a₁ → f.mk' a₁ a₂ = f.mk' b₁ b₂
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_div_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a / x) '' Set.Iic b = Set.Ici (a / b)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {s : Set E} (iso : E ≃L[𝕜] F), DifferentiableWithinAt 𝕜 (⇑iso) s x
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_sSup : ∀ {G : Type u_1} [inst : AddGroup G] {Hs : Set (AddSubgroup G)}, (∀ H ∈ Hs, H.Characteristic) → (sSup Hs).Characteristic
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isMatch_iff_isMatch_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch p pos ↔ String.Slice.Pattern.Model.IsMatch (fun x => decide (p x)) pos
-- Mathlib.Data.Int.GCD
Nat.gcdA_zero_left : ∀ {s : ℕ}, Nat.gcdA 0 s = 0
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Divisors are invariant under translation.  -/
MeromorphicOn.divisor_comp_add_const_eq_divisor : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c x : 𝕜} {f : 𝕜 → E},
  (MeromorphicOn.divisor (f ∘ fun x => x + c) U) (x - c) = (MeromorphicOn.divisor f (U + {c})) x
-- Mathlib.GroupTheory.Perm.Fin
finRotate_succ_eq_decomposeFin : ∀ {n : ℕ}, finRotate n.succ = Equiv.Perm.decomposeFin.symm (1, finRotate n)
-- Mathlib.Order.ModularLattice
inf_strictMonoOn_Icc_sup : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a b : α}, StrictMonoOn (fun c => a ⊓ c) (Set.Icc b (a ⊔ b))
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.norm_integralAgainstBilinLM_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂} {f : ContDiffMapSupportedIn E F₁ n K},
  ‖(ContDiffMapSupportedIn.integralAgainstBilinLM B μ φ) f‖ ≤
    (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f
-- Mathlib.Tactic.Conv
/-- The command `#conv tac => e` will run a conv tactic `tac` on `e`, and display the resulting
expression (discarding the proof).
For example, `#conv rw [true_and_iff] => True ∧ False` displays `False`.
There are also shorthand commands for several common conv tactics:

* `#whnf e` is short for `#conv whnf => e`
* `#simp e` is short for `#conv simp => e`
* `#norm_num e` is short for `#conv norm_num => e`
* `#push c => e` is short for `#conv push c => e`
 -/
Mathlib.Tactic.Conv.«command#conv_=>_» : Lean.ParserDescr
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorphOfContinuousClosed_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e), ⇑(e.toHomeomorphOfContinuousClosed h₁ h₂) = ⇑e
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialInsert.eq_2 : ∀ (a b : ℕ) (l : List ℕ),
  SimplexCategoryGenRel.simplicialInsert a (b :: l) =
    if a < b then a :: b :: l else b :: SimplexCategoryGenRel.simplicialInsert (a + 1) l
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.conjStarAlgEquiv_apply_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (e : H ≃ₗᵢ[𝕜] K) (x : H →L[𝕜] H) (y : K), (e.conjStarAlgEquiv x) y = e (x (e.symm y))
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_eq_of_dvd_sub_right : ∀ {α : Type u_1} [inst : CommRing α] [inst_1 : NormalizedGCDMonoid α] {a b c : α}, a ∣ b - c → gcd a b = gcd a c
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.map_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a}, Std.ExtDHashMap.map f m = ∅ ↔ m = ∅
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.summable_exp_neg_nat : Summable fun n => Real.exp (-↑n)
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- **Alias** of `Metric.Snowflaking.preimage_ofSnowflaking_eball`. -/
Metric.Snowflaking.preimage_ofSnowflaking_emetricBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : X) (r : ENNReal),
  ⇑Metric.Snowflaking.ofSnowflaking ⁻¹' Metric.eball x r = Metric.eball (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.noConfusionType : Sort v✝ → Lean.Lsp.SymbolKind → Lean.Lsp.SymbolKind → Sort v✝
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.hComp_iso_hom_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆]
  (T₁ : CategoryTheory.Functor C₁ C₂) (T₂ : CategoryTheory.Functor C₂ C₃) (V₁ : CategoryTheory.Functor C₁ C₄)
  (V₂ : CategoryTheory.Functor C₂ C₅) (V₃ : CategoryTheory.Functor C₃ C₆) (B₁ : CategoryTheory.Functor C₄ C₅)
  (B₂ : CategoryTheory.Functor C₅ C₆) [inst_6 : CategoryTheory.CatCommSq T₁ V₁ V₂ B₁]
  [inst_7 : CategoryTheory.CatCommSq T₂ V₂ V₃ B₂] (X : C₁),
  (CategoryTheory.CatCommSq.iso (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T₂ V₂ V₃ B₂).hom.app (T₁.obj X))
      (B₂.map ((CategoryTheory.CatCommSq.iso T₁ V₁ V₂ B₁).hom.app X))
-- Batteries.Data.Vector.Lemmas
Vector.back_scanl : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n},
  (Vector.scanl f init as).back = Vector.foldl f init as
-- Mathlib.Order.Cover
CovBy.eq_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, a ⋖ b → a ≤ c → c ≤ b → c = a ∨ c = b
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.swap.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousMonoidHom.swap A B = (ContinuousMonoidHom.snd A B).prod (ContinuousMonoidHom.fst A B)
-- Init.Data.Rat.Lemmas
Rat.min_def : ∀ {n m : ℚ}, min n m = if n ≤ m then n else m
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm_map_algEquiv : ∀ {A : Type u_1} {B : Type u_6} (B₂ : Type u_7) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing B₂]
  [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : IsIntegrallyClosed A] [inst_6 : IsDomain A]
  [inst_7 : IsDomain B] [inst_8 : IsIntegrallyClosed B] [inst_9 : Algebra.IsIntegral A B]
  [inst_10 : Module.IsTorsionFree A B] [inst_11 : IsDomain B₂] [inst_12 : IsIntegrallyClosed B₂]
  [inst_13 : Algebra.IsIntegral A B₂] [inst_14 : Module.IsTorsionFree A B₂]
  [Algebra.IsAlgebraic (FractionRing A) (FractionRing B)] [Algebra.IsAlgebraic (FractionRing A) (FractionRing B₂)]
  (x : B) (σ : B ≃ₐ[A] B₂), (Algebra.intNorm A B₂) (σ x) = (Algebra.intNorm A B) x