mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernel_hom_ext : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} (e₁ e₂ : SemiNormedGrp.explicitCokernel f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) e₁ =
      CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) e₂ →
    e₁ = e₂
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.getKey? a = none
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.relStructCastSuccEquivMulStruct_apply_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n}
  (h : f.RelStruct g i.castSucc), (SSet.PtSimplex.relStructCastSuccEquivMulStruct h).map = h.map
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_mul_add : ∀ {m n : ℕ}, n ≠ 0 → (m * n + n).choose n = (m + 1) * (m * n + n - 1).choose (n - 1)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.eq_3 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.both with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_3 ()
-- Lean.Data.PersistentArray
Lean.PersistentArray.forM : {α : Type u} →
  {m : Type v → Type w} → [Monad m] → Lean.PersistentArray α → (α → m PUnit.{v + 1}) → optParam ℕ 0 → m PUnit.{v + 1}
-- Mathlib.Algebra.FreeAlgebra
/-- `FreeAlgebra R X` is a domain when `R` is an integral domain.  -/
FreeAlgebra.instIsDomain : ∀ {R : Type u_4} {X : Type u_5} [inst : CommRing R] [IsDomain R], IsDomain (FreeAlgebra R X)
-- Init.Data.Format.Instances
/-- Formats an optional value, with no expectation that the Lean parser should be able to parse the
result.

This function is usually accessed through the `ToFormat (Option α)` instance.
 -/
Option.format : {α : Type u} → [Std.ToFormat α] → Option α → Std.Format
-- Init.Data.List.Find
List.idxOf_cons_self : ∀ {α : Type u_1} {a : α} [inst : BEq α] [ReflBEq α] {l : List α}, List.idxOf a (a :: l) = 0
-- Mathlib.Analysis.RCLike.Basic
RCLike.intCast_im : ∀ {K : Type u_1} [inst : RCLike K] (n : ℤ), RCLike.im ↑n = 0
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ico : ∀ (x y : ℝ), Real.toEReal ⁻¹' Set.Ico ↑x ↑y = Set.Ico x y
-- Mathlib.Data.ENat.Basic
ENat.add_one_eq_coe_top_iff : ∀ {n : WithTop ℕ∞}, n + 1 = ↑⊤ ↔ n = ↑⊤
-- Init.SizeOf
/-- We manually define the `Lean.Name` instance because we use
an opaque function for computing the hashcode field.
 -/
Lean.Name.sizeOf : Lean.Name → ℕ
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.lifts.eq_1 : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] (f : R →+* S),
  Polynomial.lifts f = (Polynomial.mapRingHom f).rangeS
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.join_cons : ∀ {α : Type u} (s : Stream'.WSeq α) (S : Stream'.WSeq (Stream'.WSeq α)),
  (Stream'.WSeq.cons s S).join = (s.append S.join).think
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instVAdd.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  UpperSet.instVAdd = { vadd := fun a s => { carrier := (fun x => a +ᵥ x) '' ↑s, upper' := ⋯ } }
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_const_smul_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : NormedSpace 𝕜 E'] {c : 𝕜},
  c ≠ 0 → ((fun x => c • f' x) =Θ[l] g ↔ f' =Θ[l] g)
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- The counit fork is a limit provided `F` preserves it.  -/
CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizer : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {adj : F ⊣ G} →
              (A : adj.toComonad.Coalgebra) →
                [inst_2 : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] →
                  [CategoryTheory.Limits.PreservesLimit
                        (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F] →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.ComonadicityInternal.counitFork A)
-- Mathlib.GroupTheory.Commutator.Basic
/-- The set of additive commutator elements `⁅g₁, g₂⁆` in `G`.  -/
addCommutatorSet : (G : Type u_1) → [AddGroup G] → Set G
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.map_smul_eq_mul_coe : ∀ (A : Type u_2) [inst : Ring A] [inst_1 : UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (R : Type u_3)
  [inst_4 : CommSemiring R] [inst_5 : Algebra R A] [UniformContinuousConstSMul R A] (r : R),
  (UniformSpace.Completion.map fun x => r • x) = fun x => ↑((algebraMap R A) r) * x
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lid_toLinearEquiv : ∀ (R : Type uR) (A : Type uA) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ↑(Algebra.TensorProduct.lid R A) = TensorProduct.lid R A
-- Mathlib.CategoryTheory.Localization.Adjunction
/-- If `adj : G ⊣ F` is an adjunction between two categories `C₁` and `C₂` that
are equipped with localization functors `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂` with
respect to `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂`, and that
the functors `F : C₂ ⥤ C₁` and `G : C₁ ⥤ C₂` induce functors `F' : D₂ ⥤ D₁`
and `G' : D₁ ⥤ D₂` on the localized categories, then the adjunction `adj`
induces an adjunction `G' ⊣ F'`.  -/
CategoryTheory.Adjunction.localization : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [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} D₁] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                {G : CategoryTheory.Functor C₁ C₂} →
                  {F : CategoryTheory.Functor C₂ C₁} →
                    (G ⊣ F) →
                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          [L₁.IsLocalization W₁] →
                            (L₂ : CategoryTheory.Functor C₂ D₂) →
                              (W₂ : CategoryTheory.MorphismProperty C₂) →
                                [L₂.IsLocalization W₂] →
                                  (G' : CategoryTheory.Functor D₁ D₂) →
                                    (F' : CategoryTheory.Functor D₂ D₁) →
                                      [CategoryTheory.CatCommSq G L₁ L₂ G'] →
                                        [CategoryTheory.CatCommSq F L₂ L₁ F'] → G' ⊣ F'
-- Mathlib.Algebra.Lie.EngelSubalgebra
/-- A Lie subalgebra of a Noetherian Lie algebra is nilpotent
if it is contained in the Engel subalgebra of all its elements.  -/
LieSubalgebra.isNilpotent_of_forall_le_engel : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L]
  (H : LieSubalgebra R L), (∀ x ∈ H, H ≤ LieSubalgebra.engel R x) → LieRing.IsNilpotent ↥H
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instLEOffset : LE Std.Time.Hour.Offset
-- Mathlib.Data.Real.Basic
Real.instAdd : Add ℝ
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finprod_mem_union'` that requires `s ∩ mulSupport f` and
`t ∩ mulSupport f` rather than `s` and `t` to be disjoint  -/
finprod_mem_union'' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  Disjoint (s ∩ Function.mulSupport f) (t ∩ Function.mulSupport f) →
    (s ∩ Function.mulSupport f).Finite →
      (t ∩ Function.mulSupport f).Finite →
        ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSigma.match_3.splitter : (motive : (n : ℕ) → (f : Fin n → ℕ) → (i : Fin n) × Fin (f i) → Sort u_1) →
  (n : ℕ) →
    (f : Fin n → ℕ) →
      (x : (i : Fin n) × Fin (f i)) →
        ((a : ℕ) → (f : Fin (a + 1) → ℕ) → (j : Fin (f 0)) → motive a.succ f ⟨⟨0, ⋯⟩, j⟩) →
          ((n : ℕ) →
              (f : Fin (n + 1) → ℕ) →
                (i : ℕ) → (hi : i + 1 < n + 1) → (j : Fin (f ⟨i + 1, hi⟩)) → motive n.succ f ⟨⟨i.succ, hi⟩, j⟩) →
            motive n f x
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.fixedBy_mul_op_eq_empty_iff : ∀ {M : Type u_3} [inst : Monoid M] [IsLeftCancelMul M] {m : M}, MulAction.fixedBy M (MulOpposite.op m) = ∅ ↔ m ≠ 1
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- If `G` is isomorphic to `H`, then `H` is contained in `G`.  -/
SimpleGraph.Iso.isContained' : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H), H.IsContained G
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run.eq_3 : ∀ {α : Type u_1} (le : α → α → Bool) (n_1 : ℕ) (xs : { l // l.length = n_1 + 2 }),
  List.MergeSort.Internal.mergeSortTR₂.run✝ le xs =
    match List.MergeSort.Internal.splitRevInTwo xs with
    | (l, r) =>
      List.MergeSort.Internal.mergeTR (List.MergeSort.Internal.mergeSortTR₂.run'✝ le l)
        (List.MergeSort.Internal.mergeSortTR₂.run✝ le r) le
-- Mathlib.Tactic.CategoryTheory.Coherence.Basic
/-- Split the goal `α ≫ η ≫ ηs = α' ≫ η' ≫ ηs'` into `α = α'`, `η = η'`, and `ηs = ηs'`.  -/
Mathlib.Tactic.BicategoryLike.ofNormalizedEq : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.Lie.Basis.Base
LieAlgebra.Basis.baseSupp'.eq_1 : ∀ {ι : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Fintype ι] [inst_1 : Field K] [inst_2 : CharZero K]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  (b : LieAlgebra.Basis ι H) (i : ι), b.baseSupp' i = ⟨{ toFun := ⇑(b.baseSupp i), genWeightSpace_ne_bot' := ⋯ }, ⋯⟩
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The translation of TM2 statements to TM1 statements. Regular actions have direct equivalents,
but stack actions are deferred by going to the corresponding `go` state, so that we can find the
appropriate stack top.  -/
Turing.TM2to1.trNormal : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} → Turing.TM2.Stmt Γ Λ σ → Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ
-- Init.Data.Order.Lemmas
Std.min_eq_if : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] {x : Min α} [Std.LawfulOrderLeftLeaningMin α] {a b : α},
  a ⊓ b = if a ≤ b then a else b
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_bot : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S],
  (Ideal.relNorm R) ⊥ = ⊥
-- Mathlib.Topology.Compactness.CountablyCompact
isCountablyCompact_univ_iff : ∀ {E : Type u_2} [inst : TopologicalSpace E], IsCountablyCompact Set.univ ↔ CountablyCompactSpace E
-- Mathlib.Analysis.Convex.Strong
UniformConcaveOn.sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {f g : E → ℝ},
  UniformConcaveOn s φ f → UniformConvexOn s ψ g → UniformConcaveOn s (φ + ψ) (f - g)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- Given right homology data `h₁` and `h₂` for two short complexes `S₁` and `S₂`,
a `RightHomologyMapData` for a morphism `φ : S₁ ⟶ S₂`
consists of a description of the induced morphisms on the `Q` (opcycles)
and `H` (right homology) fields of `h₁` and `h₂`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ⟶ S₂) → S₁.RightHomologyData → S₂.RightHomologyData → Type v_1
-- Mathlib.Algebra.Homology.Embedding.Extend
ComplexShape.Embedding.extendFunctor.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e e_1 : c.Embedding c'),
  e = e_1 →
    ∀ (C : Type u_3) [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C], e.extendFunctor C = e_1.extendFunctor C
-- Mathlib.Analysis.Distribution.TestFunction
ContDiffMapSupportedIn.postcompCLM.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {F' : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : SMulCommClass ℝ 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace ℝ F']
  [inst_9 : NormedSpace 𝕜 F'] [inst_10 : SMulCommClass ℝ 𝕜 F'] {n : ℕ∞} {K : TopologicalSpace.Compacts E}
  [inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜] (T T_1 : F →L[𝕜] F'),
  T = T_1 → ContDiffMapSupportedIn.postcompCLM T = ContDiffMapSupportedIn.postcompCLM T_1
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_comap_comap_eq_relfinrank_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E),
  B ≤ f.fieldRange → (IntermediateField.comap f A).relfinrank (IntermediateField.comap f B) = A.relfinrank B
-- Mathlib.LinearAlgebra.Dimension.Constructions
finrank_span_eq_card : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Nontrivial R] {ι : Type u_2} [inst_5 : Fintype ι] {b : ι → M},
  LinearIndependent R b → Module.finrank R ↥(Submodule.span R (Set.range b)) = Fintype.card ι
-- Init.Data.Fin.Lemmas
Fin.castLT.congr_simp : ∀ {n m : ℕ} (i i_1 : Fin m) (e_i : i = i_1) (h : ↑i < n), i.castLT h = i_1.castLT ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_eq_one_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] {s t : Finset α},
  s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.coeff_erase_apply : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α),
  ((SkewMonoidAlgebra.erase a) f).coeff = Finsupp.erase a f.coeff
-- Lean.SubExpr
/-- Fold over the position starting at the root and heading to the leaf -/
Lean.SubExpr.Pos.foldl : {α : Type} → (α → ℕ → α) → α → Lean.SubExpr.Pos → α
-- Mathlib.Topology.Order
TopologicalSpace.generateFrom_surjective : ∀ {α : Type u}, Function.Surjective TopologicalSpace.generateFrom
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccPrelimit_zero : Order.IsSuccPrelimit 0
-- Mathlib.RingTheory.OrzechProperty
OrzechProperty.bijective_of_surjective_endomorphism : ∀ {R : Type u} [inst : Semiring R] [OrzechProperty R] {M : Type v} [inst_2 : AddCommMonoid M] [inst_3 : Module R M]
  [Module.Finite R M] (f : M →ₗ[R] M), Function.Surjective ⇑f → Function.Bijective ⇑f
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of
`μ ^ p`, where `p` is a prime that does not divide `n`. Then `P` divides `Q` modulo `p`.  -/
IsPrimitiveRoot.minpoly_dvd_mod_p : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ} [inst_3 : Fact (Nat.Prime p)],
      ¬p ∣ n →
        Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣
          Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p))
-- Lean.Meta.Basic
/-- Add entry `{ className := className, fvar := fvar }` to localInstances,
and then execute continuation `k`.  -/
Lean.Meta.withNewLocalInstance : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.Name → Lean.Expr → n α → n α
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderMaxOpposite : ∀ {α : Type u_1} {il : LE α} {im : Max α} [Std.LawfulOrderMax α], Std.LawfulOrderMin α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ext₀_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {z₁ z₂ : CochainComplex.HomComplex.Cochain F G 0},
  z₁ = z₂ ↔ ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯
-- Mathlib.Analysis.Complex.Basic
RCLike.hasSum_conj' : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜},
  HasSum (fun x => (starRingEnd 𝕜) (f x)) ((starRingEnd 𝕜) x) L ↔ HasSum f x L
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.obj).inv
-- Mathlib.Data.Finset.Pi
Finset.pi_subset : ∀ {α : Type u_1} {β : α → Type u} [inst : DecidableEq α] {s : Finset α} (t₁ t₂ : (a : α) → Finset (β a)),
  (∀ a ∈ s, t₁ a ⊆ t₂ a) → s.pi t₁ ⊆ s.pi t₂
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_iUnion : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β)
  (p : ι → Set α), ⋃ i, omegaLimit f ϕ (p i) ⊆ omegaLimit f ϕ (⋃ i, p i)
-- Std.Sat.AIG.Basic
/-- A sequence of references bundled with their AIG.
 -/
Std.Sat.AIG.RefVecEntry : (α : Type) → [DecidableEq α] → [Hashable α] → [DecidableEq α] → ℕ → Type
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.instFunLike : {μ : YoungDiagram} → FunLike (SemistandardYoungTableau μ) ℕ (ℕ → ℕ)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- A `ℝ`-basis of the mixed space of `K` that is also a `ℤ`-basis of the image of the fractional
ideal `I`.  -/
NumberField.mixedEmbedding.fractionalIdealLatticeBasis : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) →
        Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥↑↑I) ℝ (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Iic b` and monotone on `Icc b a`, then the minimum of `f` on `Iic a`
is attained at `b`.  -/
isMinOn_Iic_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  AntitoneOn f (Set.Iic b) → MonotoneOn f (Set.Icc b a) → IsMinOn f (Set.Iic a) b
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.IsCompletelyPseudoMetrizableSpace.of_completeSpace_pseudometrizable : ∀ {X : Type u_1} [inst : UniformSpace X] [CompleteSpace X] [(uniformity X).IsCountablyGenerated],
  TopologicalSpace.IsCompletelyPseudoMetrizableSpace X
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.ind : ∀ {F : Type u → Type u} [q : QPF F] (p : QPF.Fix F → Prop),
  (∀ (x : F (QPF.Fix F)), Functor.Liftp p x → p (QPF.Fix.mk x)) → ∀ (x : QPF.Fix F), p x
-- Mathlib.Data.NNReal.Defs
/-- A `MulAction` over `ℝ` restricts to a `MulAction` over `ℝ≥0`.  -/
NNReal.instMulActionOfReal : {M : Type u_1} → [MulAction ℝ M] → MulAction NNReal M
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.ext : ∀ {A : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} A} {B : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {T : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} T}
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {x y : CategoryTheory.MorphismProperty.Comma L R P Q W}, x.left = y.left → x.right = y.right → x.hom ≍ y.hom → x = y
-- Mathlib.Data.Nat.Init
/-- **Alias** of `Nat.succ_le_of_lt`. -/
LT.lt.nat_succ_le : ∀ {n m : ℕ}, n < m → n.succ ≤ m
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.chainComplex_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X : SSet} {R : C} {n : ℕ} {T : C} {f g : (X.chainComplex R).X n ⟶ T},
  (∀ (x : X.obj (Opposite.op { len := n })),
      CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) f =
        CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) g) →
    f = g
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.ext_iff : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, c = d ↔ ∀ (x y : M), c x y ↔ d x y
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_iff_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {a : α},
  a ∈ m ↔ m.contains a = true
-- Mathlib.Topology.Order.OrderClosed
Ioo_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b x : α},
  a < x → x < b → Set.Ioo a b ∈ nhds x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting a multiple of the first vector passed to `oangle` from the second vector does
not change the sign of the angle.  -/
Orientation.oangle_sign_sub_smul_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ), (o.oangle x (y - r • x)).sign = (o.oangle x y).sign
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- Given a maximal ideal `v` and an ideal `I` of `R`, `maxPowDividing` returns the maximal
power of `v` dividing `I`.  -/
IsDedekindDomain.HeightOneSpectrum.maxPowDividing : {R : Type u_1} → [inst : CommRing R] → [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R → Ideal R → Ideal R
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_zpow : ∀ {x : ℝ}, 0 ≤ x → ∀ (n : ℤ), (x ^ n).toNNReal = x.toNNReal ^ n
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Triangle inequality** for the norm.  -/
norm_add_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a + b‖ ≤ ‖a‖ + ‖b‖
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- For a valuation subring `A`, `A.unitGroup` agrees with the units of `A`.  -/
ValuationSubring.unitGroupMulEquiv : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → ↥A.unitGroup ≃* (↥A)ˣ
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_Ici : ∀ {a : ℝ}, 0 < a → Real.log '' Set.Ici a = Set.Ici (Real.log a)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.isLinearMap_of_compatibleSMul : ∀ (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂), IsLinearMap R ⇑f