mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Separable
/-- If `n ≠ 0` in `F`, then `X ^ n - a` is separable for any `a ≠ 0`.  -/
Polynomial.separable_X_pow_sub_C : ∀ {F : Type u} [inst : Field F] {n : ℕ} (a : F), ↑n ≠ 0 → a ≠ 0 → (Polynomial.X ^ n - Polynomial.C a).Separable
-- Mathlib.Order.Category.LinOrd
/-- The equivalence between `LinOrd` and itself induced by `OrderDual` both ways.  -/
LinOrd.dualEquiv : LinOrd ≌ LinOrd
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.sdiff_iUnion`. -/
Set.diff_iUnion : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β), s \ ⋃ i, t i = ⋂ i, s \ t i
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Construct a bundled `CommMonCat` from the underlying type and typeclass.  -/
CommMonCat.of : (M : Type u) → [CommMonoid M] → CommMonCat
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- An auxiliary definition used only to construct the true `NormedRing` (and `Metric`) structure
provided by `Matrix.instMetricSpaceL2Op` and `Matrix.instNormedRingL2Op`.  -/
Matrix.l2OpNormedRingAux : {𝕜 : Type u_1} → {n : Type u_3} → [RCLike 𝕜] → [Fintype n] → [DecidableEq n] → NormedRing (Matrix n n 𝕜)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The preimage of a convex cone under an `R`-linear map is a convex cone.  -/
ConvexCone.comap : {R : Type u_2} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R M] → [inst_5 : Module R N] → (M →ₗ[R] N) → ConvexCone R N → ConvexCone R M
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {Z : C} {complex : ChainComplex C ℕ}
  {projective :
    autoParam (∀ (n : ℕ), CategoryTheory.Projective (complex.X n))
      CategoryTheory.ProjectiveResolution.projective._autoParam}
  {hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology complex i} {π : complex ⟶ (ChainComplex.single₀ C).obj Z}
  {quasiIso : autoParam (QuasiIso π) CategoryTheory.ProjectiveResolution.quasiIso._autoParam}
  {complex_1 : ChainComplex C ℕ}
  {projective_1 :
    autoParam (∀ (n : ℕ), CategoryTheory.Projective (complex_1.X n))
      CategoryTheory.ProjectiveResolution.projective._autoParam}
  {hasHomology_1 : ∀ (i : ℕ), HomologicalComplex.HasHomology complex_1 i}
  {π_1 : complex_1 ⟶ (ChainComplex.single₀ C).obj Z}
  {quasiIso_1 : autoParam (QuasiIso π_1) CategoryTheory.ProjectiveResolution.quasiIso._autoParam},
  { complex := complex, projective := projective, hasHomology := hasHomology, π := π, quasiIso := quasiIso } =
      { complex := complex_1, projective := projective_1, hasHomology := hasHomology_1, π := π_1,
        quasiIso := quasiIso_1 } →
    complex = complex_1 ∧ π ≍ π_1
-- Mathlib.Order.Heyting.Basic
himp_le_himp_left : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b → c ⇨ a ≤ c ⇨ b
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.id_comp : ∀ {U : Type u_1} {V : Type u_2} [inst : CategoryTheory.ReflQuiver U] [inst_1 : CategoryTheory.ReflQuiver V]
  (F : U ⥤rq V), 𝟭rq U ⋙rq F = F
-- Std.Http.Data.Status
Std.Http.Status.found.sizeOf_spec : sizeOf Std.Http.Status.found = 1
-- Mathlib.Tactic.GCongr.ForwardAttr
Mathlib.Tactic.GCongr.ForwardExt.mk.sizeOf_spec : ∀ (eval : Lean.Expr → Lean.MVarId → Lean.MetaM Unit), sizeOf { eval := eval } = 1
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.preGNS_inner_def : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) [inst_2 : StarOrderedRing A]
  (a b : f.PreGNS), inner ℂ a b = f (star (f.ofPreGNS a) * f.ofPreGNS b)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace
      (NumberField.mixedEmbedding.fundamentalCone.completeFamily K NumberField.Units.dirichletUnitTheorem.w₀) =
    0
-- Mathlib.Topology.MetricSpace.Kuratowski
/-- The embedding map is always a semi-contraction.  -/
KuratowskiEmbedding.embeddingOfSubset_dist_le : ∀ {α : Type u} [inst : MetricSpace α] (x : ℕ → α) (a b : α),
  dist (KuratowskiEmbedding.embeddingOfSubset x a) (KuratowskiEmbedding.embeddingOfSubset x b) ≤ dist a b
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Iio_iff : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ : α}, b₁ ≤ a₁ → (Set.Icc b₁ a₁ ⊆ Set.Iio a₂ ↔ a₁ < a₂)
-- Mathlib.Order.PropInstances
Prop.disjoint_iff : ∀ {P Q : Prop}, Disjoint P Q ↔ ¬(P ∧ Q)
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The limit of a functor into a complete lattice is the infimum of the objects in the image.
 -/
CategoryTheory.Limits.CompleteLattice.limit_eq_iInf : ∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α), CategoryTheory.Limits.limit F = iInf F.obj
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote'_eq_denote : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denote' ctx p = Lean.Grind.Linarith.Poly.denote ctx p
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.ext_iff : ∀ {A : Type uA} [inst : AddCommGroup A] {c c' : CharacterModule A}, c = c' ↔ ∀ (x : A), c x = c' x
-- Init.Data.UInt.Lemmas
USize.add_left_neg : ∀ (a : USize), -a + a = 0
-- Init.Data.Vector.Lemmas
Vector.flatMap_append : ∀ {α : Type u_1} {n k : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {ys : Vector α k} {f : α → Vector β m},
  (xs ++ ys).flatMap f = Vector.cast ⋯ (xs.flatMap f ++ ys.flatMap f)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pushforward.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (R : CategoryTheory.Presieve X)
  (Z : C) (fg : Z ⟶ Y),
  CategoryTheory.Presieve.pushforward f R fg = ∃ g, CategoryTheory.CategoryStruct.comp g f = fg ∧ R g
-- Mathlib.Dynamics.FixedPoints.Defs
Function.fixedPoints_id : ∀ {α : Type u_1}, Function.fixedPoints id = Set.univ
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice_4 : {α : Type u} → Std.Roo.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.Tactic.TermCongr
/-- Given two applications of the same arity, gives `Expr.getAppFn` of both,
but if these functions are equal, gives the longest common prefix.
 -/
_private.Mathlib.Tactic.TermCongr.0.Mathlib.Tactic.TermCongr.getJointAppFns : Lean.Expr → Lean.Expr → Lean.Expr × Lean.Expr
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.mem_pretopology_iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {X : AlgebraicGeometry.Scheme} {R : CategoryTheory.Presieve X},
  R ∈ (AlgebraicGeometry.Scheme.pretopology P).coverings X ↔ ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_eq_some_getD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, a ∈ t → t.get? a = some (t.getD a fallback)
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.getModifiersForLetRecs : Array Lean.Elab.DefViewElabHeader → Lean.Elab.Modifiers
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U],
  CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F =
    CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.neg_vadd_set_distrib : ∀ {α : Type u_2} [inst : AddGroup α] (a : α) (s : Set α), -(a +ᵥ s) = AddOpposite.op (-a) +ᵥ -s
-- Lean.Data.PersistentArray
Lean.instInhabitedPersistentArrayNode : {a : Type u_1} → Inhabited (Lean.PersistentArrayNode a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDeclarationParams.fromJson : Lean.Json → Except String Lean.Lsp.DeclarationParams
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheaf.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ Φ_1 : J.Point),
  Φ = Φ_1 →
    ∀ {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
      (M M_1 : A), M = M_1 → Φ.skyscraperPresheaf M = Φ_1.skyscraperPresheaf M_1
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- **Alias** of `FunLike.coe_add`. -/
MeasureTheory.OuterMeasure.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Data.Finset.Defs
Finset.mk.injEq : ∀ {α : Type u_4} (val : Multiset α) (nodup : val.Nodup) (val_1 : Multiset α) (nodup_1 : val_1.Nodup),
  ({ val := val, nodup := nodup } = { val := val_1, nodup := nodup_1 }) = (val = val_1)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- Constructor for isomorphisms between 1-morphisms in the bicategory `Adj B`.  -/
CategoryTheory.Bicategory.Adj.iso₂Mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} →
      {α β : a ⟶ b} →
        (el : α.l ≅ β.l) →
          (er : β.r ≅ α.r) →
            autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) el.hom = er.hom)
                CategoryTheory.Bicategory.Adj.iso₂Mk._auto_1 →
              (α ≅ β)
-- Std.Tactic.Do.Syntax
Lean.Elab.Tactic.Do.VCGen.Config.mk.injEq : ∀ (trivial leave elimLets jp : Bool) (stepLimit : Option ℕ)
  (errorOnMissingSpec debug internalize trivial_1 leave_1 elimLets_1 jp_1 : Bool) (stepLimit_1 : Option ℕ)
  (errorOnMissingSpec_1 debug_1 internalize_1 : Bool),
  ({ trivial := trivial, leave := leave, elimLets := elimLets, jp := jp, stepLimit := stepLimit,
        errorOnMissingSpec := errorOnMissingSpec, debug := debug, internalize := internalize } =
      { trivial := trivial_1, leave := leave_1, elimLets := elimLets_1, jp := jp_1, stepLimit := stepLimit_1,
        errorOnMissingSpec := errorOnMissingSpec_1, debug := debug_1, internalize := internalize_1 }) =
    (trivial = trivial_1 ∧
      leave = leave_1 ∧
        elimLets = elimLets_1 ∧
          jp = jp_1 ∧
            stepLimit = stepLimit_1 ∧
              errorOnMissingSpec = errorOnMissingSpec_1 ∧ debug = debug_1 ∧ internalize = internalize_1)
-- Mathlib.Algebra.GroupWithZero.Defs
MulZeroClass.toZero : {M₀ : Type u} → [self : MulZeroClass M₀] → Zero M₀
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- From a functor `F : J ⥤ C`, given an initial object of `J`, construct a cocone for `J`,
provided that the morphisms in the diagram are isomorphisms.
In `colimitOfDiagramInitial` we show it is a colimit cocone.  -/
CategoryTheory.Limits.coconeOfDiagramInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {X : J} →
          CategoryTheory.Limits.IsInitial X →
            (F : CategoryTheory.Functor J C) →
              [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] → CategoryTheory.Limits.Cocone F
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_inverse_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  {X Y : CategoryTheory.CommGrp C} (f : X ⟶ Y),
  CategoryTheory.Preadditive.commGrpEquivalence.inverse.map f = f.hom.hom.hom
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformContinuous_postcomp' : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] {β : ι → Type u_4}
  [inst : (i : ι) → UniformSpace (β i)] {g : (i : ι) → α i → β i},
  (∀ (i : ι), UniformContinuous (g i)) → UniformContinuous fun f i => g i (f i)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.toCostructuredArrow_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) (X : F.Elementsᵒᵖ),
  (CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X =
    CategoryTheory.CostructuredArrow.mk (CategoryTheory.yonedaEquiv.symm (Opposite.unop X).snd)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {f : α → Bool} {k : α},
  (Std.DTreeMap.filter (fun k x => f k) t).getKey! k = (Option.filter f (t.getKey? k)).get!
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.obj'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F F_1 : CategoryTheory.ComposableArrows C n),
  F = F_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (hi : i ≤ n), F.obj' i hi = F_1.obj' i_1 ⋯
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  (m.erase k).contains a = (!k == a && m.contains a)
-- Mathlib.Data.ZMod.Units
ZMod.coe_int_mul_inv_eq_one : ∀ {n : ℕ} {x : ℤ}, IsCoprime x ↑n → ↑x * (↑x)⁻¹ = 1
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.clift_apply_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : FreeMonoid (M ⊕ N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1)
  (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y)))
  (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y)))
  (x : N), (Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inr x) = f (FreeMonoid.of (Sum.inr x))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isCycle₁_of_mem_cycles₁ : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ x ∈ groupHomology.cycles₁ (Rep.ofDistribMulAction k G A), groupHomology.IsCycle₁ x
-- Mathlib.RingTheory.IsGaloisGroup.Basic
IsGaloisGroup.mulEquivAlgEquiv_apply_symm_apply : ∀ (G : Type u_1) [inst : Group G] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : FaithfulSMul A B] [inst_6 : MulSemiringAction G B]
  [inst_7 : IsGaloisGroup G A B] [inst_8 : Finite G] (a : G) (a_1 : B),
  ((IsGaloisGroup.mulEquivAlgEquiv G A B) a).symm a_1 = a⁻¹ • a_1
-- Mathlib.RingTheory.Derivation.DifferentialRing
DifferentialAlgebra.mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Differential A] [inst_4 : Differential B],
  (∀ (a : A), ((algebraMap A B) a)′ = (algebraMap A B) a′) → DifferentialAlgebra A B
-- Mathlib.Probability.Independence.Integration
/-- If `X` and `Y` are two independent random variables, `B X Y` is integrable, `X` is not
almost-surely `0` and `c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ`, then `Y` is integrable.

This is useful for the case where `B` is scalar multiplication, as it will allow to drop
integrability hypotheses.  -/
ProbabilityTheory.IndepFun.integrable_right_of_integrable_op : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : NormedAddGroup E] [inst_1 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_3 : TopologicalSpace F]
  [inst_4 : ContinuousENorm F] [inst_5 : MeasurableSpace F] [OpensMeasurableSpace F] [inst_7 : TopologicalSpace G]
  [inst_8 : ContinuousENorm G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    ∀ (B : E → F → G) (c : NNReal),
      c ≠ 0 →
        (∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ) →
          MeasureTheory.Integrable (fun ω => B (X ω) (Y ω)) μ →
            MeasureTheory.AEStronglyMeasurable X μ →
              MeasureTheory.AEStronglyMeasurable Y μ → ¬X =ᵐ[μ] 0 → MeasureTheory.Integrable Y μ
-- Mathlib.Data.ZMod.Basic
ZMod.val_natCast_of_lt : ∀ {n a : ℕ}, a < n → (↑a).val = a
-- Mathlib.Algebra.Group.Units.Equiv
Group.mulLeft_bijective : ∀ {G : Type u_5} [inst : Group G] (a : G), Function.Bijective fun x => a * x
-- Mathlib.Algebra.Lie.CartanCriterion
/-- **Cartan's criterion for solvability**: if the Killing form of `L` vanishes on `L × ⁅L, L⁆`,
then `L` is solvable.  -/
LieAlgebra.isSolvable_of_killingForm_apply_lie_eq_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [CharZero R] [IsDomain R] [inst_3 : LieRing L]
  [inst_4 : LieAlgebra R L] [IsNoetherian R L] [Module.Free R L],
  (∀ (x y : L), y ∈ LieAlgebra.derivedSeries R L 1 → ((killingForm R L) x) y = 0) → LieAlgebra.IsSolvable L
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.mul_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : One M] [inst_1 : One N] [inst_2 : MulOneClass P]
  (g₁ g₂ : OneHom N P) (f : OneHom M N), (g₁ * g₂).comp f = g₁.comp f * g₂.comp f
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.equiv.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I I_1 : ModelWithCorners 𝕜 E H}
  (e_I : I = I_1) {J J_1 : ModelWithCorners 𝕜 E'' G} (e_J : J = J_1) {M : Type u_11} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N]
  {n n_1 : WithTop ℕ∞} (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M} (e_x : x = x_1)
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), h.equiv = ⋯.equiv
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued.congr_simp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d d_1 : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰),
  d = d_1 →
    ∀
      [inst_5 :
        ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
          CategoryTheory.Limits.PreservesColimitsOfShape J
            (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
      [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀]
      [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P], d.glued = d_1.glued
-- Mathlib.Order.Disjoint
disjoint_left_comm : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b c : α}, Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNewUnit.eq_1 : ∀ {α : Type u} [inst : BEq α] (l : List ((_ : α) × Unit)), Std.Internal.List.insertListIfNewUnit l [] = l
-- Mathlib.Topology.Order.Rolle
/-- If a function `f` is continuous on an open interval
and tends to the same value at its endpoints, then it has an extremum on this open interval.  -/
exists_isExtrOn_Ioo_of_tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X} {l : Y},
  a < b →
    ContinuousOn f (Set.Ioo a b) →
      Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
        Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l) → ∃ c ∈ Set.Ioo a b, IsExtrOn f (Set.Ioo a b) c
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.strictConcaveOn_negMulLog : StrictConcaveOn ℝ (Set.Ici 0) Real.negMulLog
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.slice.inj : ∀ {numPrefix numSuffix numPrefix_1 numSuffix_1 : ℕ},
  Lean.Elab.Term.Quotation.HeadCheck.slice numPrefix numSuffix =
      Lean.Elab.Term.Quotation.HeadCheck.slice numPrefix_1 numSuffix_1 →
    numPrefix = numPrefix_1 ∧ numSuffix = numSuffix_1
-- Init.Data.List.ToArray
Array.swap_def : ∀ {α : Type u_1} (xs : Array α) (i j : ℕ) (hi : i < xs.size) (hj : j < xs.size),
  xs.swap i j hi hj = (xs.set i xs[j] hi).set j xs[i] ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k k' fallback : α},
      cmp k k' = Ordering.eq →
        k ∉ t →
          List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
            k ∈ l → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKeyD k' fallback = k
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.insertPerm.match_1.eq_2 : ∀ (motive : (x : ℕ) → Fin2 x → Fin2 x → Sort u_1) (n : ℕ) (j : Fin2 n) (h_1 : (n : ℕ) → motive (n + 1) Fin2.fz Fin2.fz)
  (h_2 : (n : ℕ) → (j : Fin2 n) → motive (n + 1) Fin2.fz j.fs)
  (h_3 : (a : ℕ) → (a_1 : Fin2 a.succ) → motive (a.succ + 1) a_1.fs Fin2.fz)
  (h_4 : (a : ℕ) → (i : Fin2 a.succ) → (j : Fin2 (a + 1)) → motive (a.succ + 1) i.fs j.fs),
  (match n + 1, Fin2.fz, j.fs with
    | .(n + 1), Fin2.fz, Fin2.fz => h_1 n
    | .(n + 1), Fin2.fz, j.fs => h_2 n j
    | .(a.succ + 1), a_1.fs, Fin2.fz => h_3 a a_1
    | .(a.succ + 1), i.fs, j.fs => h_4 a i j) =
    h_2 n j
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.ne_endPos_of_singleton : ∀ {t₁ : String} {c : Char} {t₂ : String} {s : String.Slice} {p : s.Pos},
  p.Splits t₁ (String.singleton c ++ t₂) → p ≠ s.endPos
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.mem_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.Equiv m₂ → (k ∈ m₁ ↔ k ∈ m₂)
-- Mathlib.Topology.Algebra.UniformConvergence
instOneUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [One β] → One (UniformOnFun α β 𝔖)
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.linearIndependent_single_of_ne_zero : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [IsDomain R]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] {v : ι → M},
  (∀ (i : ι), v i ≠ 0) → LinearIndependent R fun i => fun₀ | i => v i
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_union_of_disjoint : ∀ {α : Type u} {S T : Set α}, Disjoint S T → Cardinal.mk ↑(S ∪ T) = Cardinal.mk ↑S + Cardinal.mk ↑T
-- Init.Data.Sum.Basic
Sum.lex_inr_inl : ∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {b : β} {a : α},
  ¬Sum.Lex r s (Sum.inr b) (Sum.inl a)