mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.mkEMatchTheoremWithKind?.go : Lean.Meta.Grind.Origin →
  Array Lean.Name →
    Lean.Expr →
      Lean.Meta.Grind.EMatchTheoremKind →
        Lean.Meta.Grind.SymbolPriorities →
          Bool → Bool → Bool → Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Option Lean.Meta.Grind.EMatchTheorem)
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.max_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (S T : CategoryTheory.Subfunctor F) (i : C), (S ⊔ T).obj i = S.obj i ∪ T.obj i
-- Mathlib.Order.Filter.Basic
/-- **Alias** of the reverse direction of `Filter.frequently_inf_principal`. -/
Filter.Frequently.inf_principal : ∀ {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop},
  (∃ᶠ (x : α) in f, x ∈ s ∧ p x) → ∃ᶠ (x : α) in f ⊓ Filter.principal s, p x
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.mk : ℤ → Lean.Omega.Coeffs → Lean.Omega.LinearCombo
-- Batteries.Tactic.Congr
_private.Batteries.Tactic.Congr.0.Batteries.Tactic.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Batteries.Tactic.Congr.Config
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquivOfAlgEquiv_symm_apply : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} (S : Type u_6) [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] [inst_7 : IsLocalization M S] {P : Type u_7} [inst_8 : CommSemiring P]
  [inst_9 : Algebra A P] {T : Submonoid P} (Q : Type u_8) [inst_10 : CommSemiring Q] [inst_11 : Algebra A Q]
  [inst_12 : Algebra P Q] [inst_13 : IsScalarTower A P Q] [inst_14 : IsLocalization T Q] (h : R ≃ₐ[A] P)
  (H : Submonoid.map h M = T) (a : Q),
  (IsLocalization.algEquivOfAlgEquiv S Q h H).symm a =
    (IsLocalization.map S ↑{ toEquiv := ↑h.symm, map_mul' := ⋯, map_add' := ⋯ } ⋯) a
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- A non-unital subsemiring `S` includes `closure s` if and only if it includes `s`.  -/
NonUnitalSubsemiring.closure_le : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {t : NonUnitalSubsemiring R},
  NonUnitalSubsemiring.closure s ≤ t ↔ s ⊆ ↑t
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_bijective : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G},
  Function.Bijective Rep.Hom.hom
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.instMonadWithReaderOfSubExprDelabM : MonadWithReaderOf Lean.SubExpr Lean.PrettyPrinter.Delaborator.DelabM
-- Mathlib.Algebra.Group.Action.End
/-- `Function.End.applyMulAction` is faithful.  -/
Function.End.apply_FaithfulSMul : ∀ {α : Type u_5}, FaithfulSMul (Function.End α) α
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquiv.eq_1 : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [h : Algebra.IsPushout R S A B],
  KaehlerDifferential.tensorKaehlerEquiv R S A B =
    {
      toAddHom :=
        (↑(((LinearEquiv.restrictScalars R
                      (((TensorProduct.AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm)
                                (LinearEquiv.refl A Ω[A⁄R])).trans
                            (TensorProduct.comm A (TensorProduct R A S) Ω[A⁄R])).trans
                        (TensorProduct.AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S))).trans
                  (TensorProduct.comm R Ω[A⁄R] S)).trans
              (LinearEquiv.restrictScalars R (KaehlerDifferential.tensorKaehlerEquivBase R S A B)))).toAddHom,
      map_smul' := ⋯,
      invFun :=
        (((LinearEquiv.restrictScalars R
                    (((TensorProduct.AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm)
                              (LinearEquiv.refl A Ω[A⁄R])).trans
                          (TensorProduct.comm A (TensorProduct R A S) Ω[A⁄R])).trans
                      (TensorProduct.AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S))).trans
                (TensorProduct.comm R Ω[A⁄R] S)).trans
            (LinearEquiv.restrictScalars R (KaehlerDifferential.tensorKaehlerEquivBase R S A B))).invFun,
      left_inv := ⋯, right_inv := ⋯ }
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedCtorView.default : Lean.Elab.Command.CtorView
-- Mathlib.Order.Atoms
SetLike.isAtom_iff : ∀ {A : Type u_4} {B : Type u_5} [inst : PartialOrder A] [inst_1 : SetLike A B] [IsConcreteLE A B] [inst_3 : OrderBot A]
  {K : A}, IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- Upper bound for the sections of `Precoverage.subsheafify`: If for every `X : C`,
the underlying type of `𝒮 X` embeds into `ι X`, the sections of `K.subsheafify 𝒮`
on `X` embed into `Witness K ι X`.  -/
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → (C → Type w) → C → Type (max w u v)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruImage (F.map f))
      (CategoryTheory.Abelian.PreservesImage.iso F f).inv =
    F.map (CategoryTheory.Abelian.factorThruImage f)
-- Mathlib.NumberTheory.LucasLehmer
/-- Version of `sMod` that is `ℕ`-valued. One should have `q = 2 ^ p - 1`.
This can be reduced by the kernel.  -/
LucasLehmer.norm_num_ext.sModNat : ℕ → ℕ → ℕ
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w : Fin (n + 1) → R},
  ∑ j, w j = 1 →
    ∀ {i : Fin (n + 1)},
      (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide (s.points i)
          ((Finset.affineCombination R Finset.univ s.points) w) ↔
        0 < w i
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.isometry_extend : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] (f : α ↪ δ) (h : BoundedContinuousFunction δ β),
  Isometry fun g => BoundedContinuousFunction.extend f g h
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- Every entry of a doubly stochastic matrix is less than or equal to 1.  -/
le_one_of_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n → ∀ {i j : n}, M i j ≤ 1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- The set of vertices of `G` making up the connected component `C`  -/
SimpleGraph.ComponentCompl.supp : {V : Type u} → {G : SimpleGraph V} → {K : Set V} → G.ComponentCompl K → Set V
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The middle right map in the reverse hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₂ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂' C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ C
-- Mathlib.Algebra.Opposites
AddOpposite.op_vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd α β] (a : α) (b : β), AddOpposite.op (a +ᵥ b) = a +ᵥ AddOpposite.op b
-- Lean.Meta.Tactic.Grind.AC.Types
/-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal.  -/
Lean.Meta.Grind.AC.Struct.denoteEntries : Lean.Meta.Grind.AC.Struct → Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)
-- Init.Data.List.Sublist
List.infix_concat : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂ → l₁ <:+: l₂.concat a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vlt_mul_of_vle_of_vlt : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {a b c d : R}, a ≤ᵥ b → c <ᵥ d → 0 <ᵥ a → a * c <ᵥ b * d
-- Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree
ContinuousCohomology.mem_const_resol₀ : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G),
  ∀ x ∈ X.ρ.invariants, ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants
-- Mathlib.Logic.Basic
instCommutativeXor : Std.Commutative Xor
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_monomial : ∀ {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R] {f : σ → R},
  (MvPolynomial.eval f) ((MvPolynomial.monomial s) a) = a * s.prod fun n e => f n ^ e
-- Mathlib.Order.Interval.Set.InitialSeg
/-- `Iic j` is an initial segment.  -/
Set.initialSegIic : {α : Type u_1} → [inst : Preorder α] → (j : α) → ↑(Set.Iic j) ≤i α
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
/-- **Alias** of `mfderiv_prodMk`. -/
MDifferentiableAt.mfderiv_prod : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {x : M} {f : M → M'} {g : M → M''},
  MDiffAt f x → MDiffAt g x → (mfderiv% fun x => (f x, g x)) x = (mfderiv% f x).prod (mfderiv% g x)
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
/-- If `f` is integrable with respect to `Measure.sum μ`, then the sequence
`fun i ↦ ∫ x, f x ∂μ i` is summable and its sum is `∫ x, f x ∂Measure.sum μ`.  -/
MeasureTheory.hasSum_integral_measure : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {μ : ι → MeasureTheory.Measure X} {f : X → E} [inst_1 : NormedSpace ℝ E],
  MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ) →
    HasSum (fun i => ∫ (x : X), f x ∂μ i) (∫ (x : X), f x ∂MeasureTheory.Measure.sum μ)
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.of_sups_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α}, (s ⊻ t).Nonempty → s.Nonempty
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_rco : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LE α]
  [inst_5 : LT α] [inst_6 : DecidableLT α] [inst_7 : Std.PRange.UpwardEnumerable α] [inst_8 : Std.Rxo.IsAlwaysFinite α]
  [inst_9 : Std.PRange.LawfulUpwardEnumerable α] [inst_10 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_11 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Rco α} {init : β} {f : α → β → m (ForInStep β)}
  (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.comp_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A A' A'' : T.Algebra}
  (f : A ⟶ A') (g : A' ⟶ A''), (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The sieve of `X : C` that is generated by a family of objects `Y : I → C`:
it consists of morphisms `p : Z ⟶ X` such that there exists a morphism `Z ⟶ Y i`
for some `i` (note that this does not depend on `p`, only on the object `Z`).  -/
CategoryTheory.Sieve.ofObjects : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {I : Type u_1} → (I → C) → (X : C) → CategoryTheory.Sieve X
-- Mathlib.Analysis.Normed.Group.AddTorsor
uniformContinuous_vadd : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P], UniformContinuous fun x => x.1 +ᵥ x.2
-- Mathlib.Data.Multiset.UnionInter
Multiset.filter_union : ∀ {α : Type u_1} [inst : DecidableEq α] (p : α → Prop) [inst_1 : DecidablePred p] (s t : Multiset α),
  Multiset.filter p (s ∪ t) = Multiset.filter p s ∪ Multiset.filter p t
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.coe_iInf : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Sort u_3}
  (S : ι → IntermediateField F E), ↑(iInf S) = ⋂ i, ↑(S i)
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.slope_lt_rightDeriv : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConcaveOn ℝ S f →
    x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f (Set.Ioi x) x → slope f x y < derivWithin f (Set.Ioi x) x
-- Init.Data.Nat.ToString
Nat.ofDigitChars_toDigits : ∀ {b n : ℕ}, 1 < b → b ≤ 10 → b.ofDigitChars (b.toDigits n) 0 = n
-- Mathlib.Data.Sym.Basic
SymOptionSuccEquiv.decode.eq_2 : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n.succ),
  SymOptionSuccEquiv.decode (Sum.inr s) = Sym.map (⇑Function.Embedding.some) s
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.isDominant_comp_hom : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f : X.PartialMap Y)
  [inst_2 : AlgebraicGeometry.IsDominant f.hom] (g : Y.PartialMap Z) [AlgebraicGeometry.IsDominant g.hom],
  AlgebraicGeometry.IsDominant (f.comp g).hom
-- Mathlib.Data.List.Triplewise
List.Triplewise.below.cons : ∀ {α : Type u_1} {p : α → α → α → Prop} {motive : (a : List α) → List.Triplewise p a → Prop} {a : α} {l : List α}
  (a_1 : List.Pairwise (p a) l) (a_2 : List.Triplewise p l),
  List.Triplewise.below a_2 → motive l a_2 → List.Triplewise.below ⋯
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleDocumentColor : Lean.Lsp.DocumentColorParams → Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.ColorInformation))
-- Init.Data.UInt.Lemmas
UInt64.one_mul : ∀ (a : UInt64), 1 * a = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.eraseMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {l : List α}, (↑(t₁.eraseMany! l)).Equiv ↑(t₂.eraseMany! l)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β), m = m_1 → m.size = m_1.size
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.instIsMonHomInvHomOfIsCommMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M G : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.GrpObj G] [inst_4 : CategoryTheory.BraidedCategory C]
  [CategoryTheory.IsCommMonObj G] {f : M ⟶ G} [CategoryTheory.IsMonHom f], CategoryTheory.IsMonHom f⁻¹
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.det_vandermonde_ne_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [IsDomain R] {v : Fin n → R},
  (Matrix.vandermonde v).det ≠ 0 ↔ Function.Injective v
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Iic b` and antitone on `Ici b`, then the maximum of `f` is attained
at `b`.  -/
isMaxOn_univ_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {b : α} {f : α → β},
  MonotoneOn f (Set.Iic b) → AntitoneOn f (Set.Ici b) → IsMaxOn f Set.univ b
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.hb : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (self : FermatLastTheoremForThreeGen.Solution'✝ hζ),
  ¬hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution'.b✝ self
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.toMonoidal_toLaxMonoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (h : F.CoreMonoidal), h.toMonoidal.toLaxMonoidal = h.toLaxMonoidal
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_le_fp : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Monotone f → ∀ {a b : Ordinal.{u}}, a ≤ b → f b ≤ b → Ordinal.nfp f a ≤ b
-- Lean.Data.Lsp.Diagnostics
/-- Additional metadata about the diagnostic.  -/
Lean.Lsp.DiagnosticWith.tags? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option (Array Lean.Lsp.DiagnosticTag)
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.finrank_subsingleton : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Subsingleton R],
  Module.finrank R M = 1
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.fstCLM_apply : ∀ (R : Type u_3) (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (x : TrivSqZeroExt R M), (TrivSqZeroExt.fstCLM R M) x = x.fst
-- Mathlib.Algebra.GroupWithZero.Divisibility
/-- `DvdNotUnit a b` expresses that `a` divides `b` "strictly", i.e. that `b` divided by `a`
is not a unit.  -/
DvdNotUnit : {α : Type u_1} → [CommMonoidWithZero α] → α → α → Prop
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData_left : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData K e hj' hi hi' hk hk' h).left =
    HomologicalComplex.extend.leftHomologyData K e hj' hi hi' hk hk' h.left
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.matrix_bot : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocRing R] [inst_1 : Fintype n], TwoSidedIdeal.matrix n ⊥ = ⊥
-- Mathlib.Algebra.Algebra.Tower
Submodule.coe_span_eq_span_of_surjective : ∀ (R : Type u) (A : Type w) {M : Type v₁} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [IsScalarTower R A M],
  Function.Surjective ⇑(algebraMap R A) → ∀ (s : Set M), ↑(Submodule.span A s) = ↑(Submodule.span R s)
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_pi_le_of_le`. -/
EMetric.diam_pi_le_of_le : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (X i)]
  {s : (i : ι) → Set (X i)} {c : ENNReal}, (∀ (b : ι), Metric.ediam (s b) ≤ c) → Metric.ediam (Set.univ.pi s) ≤ c
-- Mathlib.Algebra.Group.Opposite
AddOpposite.op_nsmul : ∀ {α : Type u_1} [inst : AddMonoid α] (x : α) (n : ℕ), AddOpposite.op (n • x) = n • AddOpposite.op x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySum_convex : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (B : ℝ),
  Convex ℝ (NumberField.mixedEmbedding.convexBodySum K B)
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_fun_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 g s x → derivWithin (fun y => f y + g y) s x = derivWithin f s x + derivWithin g s x
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A normed ring is a ring endowed with a norm which satisfies the inequality `‖x y‖ ≤ ‖x‖ ‖y‖`.  -/
NormedRing : Type u_5 → Type u_5
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.comp_assoc : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} {M₄ : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄]
  {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} {B₃ : LinearMap.BilinForm R M₃}
  {B₄ : LinearMap.BilinForm R M₄} (h : B₃ →bᵢ B₄) (g : B₂ →bᵢ B₃) (f : B₁ →bᵢ B₂), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.Data.Set.Prod
Set.offDiag_insert : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C],
  CategoryTheory.Limits.PreservesFiniteColimits
    (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding F)
-- Lean.Meta.ArgsPacker
/-- Given a (dependent) tuple `t` (using `PSigma`) of the given arity.
Return an array containing its "elements".
Example: `mkTupleElems a 4` returns `#[a.1, a.2.1, a.2.2.1, a.2.2.2]`.
 -/
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Unary.mkTupleElems : Lean.Expr → ℕ → Array Lean.Expr
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.app_unitForward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (X : Cᵒᵖ)
  (p :
    CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η)
      (Opposite.unop X)),
  (CategoryTheory.ConcreteCategory.hom (η.app X)) (CategoryTheory.OverPresheafAux.unitForward η (Opposite.unop X) p) =
    p.yonedaEquivFst