mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Units.Basic
mul_inv_eq_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, b ≠ 0 → (a * b⁻¹ = 1 ↔ a = b)
-- Mathlib.CategoryTheory.Limits.EpiMono
CategoryTheory.mono_iff_isIso_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y}
  {c : CategoryTheory.Limits.PullbackCone f f} (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.snd
-- Mathlib.Data.Setoid.Partition
Setoid.Partitions.isPartition : ∀ {α : Type u_1} (p : Setoid.Partitions α), Setoid.IsPartition p.toSet
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toSubgroup_comap : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : Group N]
  [inst_3 : TopologicalSpace N] (H : OpenSubgroup N) (f : G →* N) (hf : Continuous ⇑f),
  ↑(OpenSubgroup.comap f hf H) = Subgroup.comap f ↑H
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.instFaithfulCommaForget : ∀ {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) [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative], (CategoryTheory.MorphismProperty.Comma.forget L R P Q W).Faithful
-- Std.Sync.StreamMap
/-- Check if a stream with the given name exists
 -/
Std.StreamMap.contains : {α β : Type} → [BEq α] → Std.StreamMap α β → α → Bool
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.diam_boxIcc : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] (ν : ι → ℤ),
  Metric.diam (BoxIntegral.Box.Icc (BoxIntegral.unitPartition.box n ν)) ≤ 1 / ↑n
-- Batteries.Lean.Meta.UnusedNames
/-- Auxiliary definition for `getUnusedUserNames`.  -/
_private.Batteries.Lean.Meta.UnusedNames.0.Lean.LocalContext.getUnusedUserNames.loop : Lean.Name → Array Lean.Name → ℕ → ℕ → Array Lean.Name
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.instMonoidalOfNatNatCatHoFunctor₂ : SSet.Truncated.hoFunctor₂.Monoidal
-- Mathlib.RingTheory.Valuation.ValuationRing
/-- An integral domain is called a `ValuationRing` provided that for any pair
of elements `a b : A`, either `a` divides `b` or vice versa.  -/
ValuationRing : (A : Type u) → [inst : CommRing A] → [IsDomain A] → Prop
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.addUnresolvedCompletionItemForDecl : Lean.Name → Lean.Name → Lean.Server.Completion.M✝ Unit
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f) (hf' : IsOpenMap f) (s : TopologicalSpace.PositiveCompacts α),
  ↑(TopologicalSpace.PositiveCompacts.map f hf hf' s) = f '' ↑s
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
/-- The polarization map from weight space to coweight space as an equivalence.  -/
RootPairing.PolarizationEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Fintype ι] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : Field R] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] → (P : RootPairing ι R M N) → [P.IsAnisotropic] → [P.IsRootSystem] → M ≃ₗ[R] N
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E},
  s =ᶠ[nhds x] t → VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracketWithin 𝕜 V W t x
-- Mathlib.Order.BooleanAlgebra.Basic
inf_sdiff_distrib_left : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (a b c : α), a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
-- Mathlib.Order.Booleanisation
Booleanisation.LT.sep : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α},
  Disjoint a b → (Booleanisation.lift a).LT (Booleanisation.comp b)
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.coe_injective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {H' : Type u_5} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  ⦃f g : ContMDiffMap I I' M M' n⦄, ⇑f = ⇑g → f = g
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.DecEq_eq : ∀ {α : Type u_1} [inst : DecidableEq α], List.instBEq = instBEqOfDecidableEq
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
AddSubgroup.eq_bot_or_eq_top_of_prime_card : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G) [hp : Fact (Nat.Prime (Nat.card G))], H = ⊥ ∨ H = ⊤
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.isMulCommutative_adjoin_singleton : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (x : A),
  IsMulCommutative ↥(NonUnitalAlgebra.adjoin R {x})
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.WeaklyEtale
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.snd_convexCombPair : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {X : Type u_3}
  {Y : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] (a b : R) (ha : 0 ≤ a)
  (hb : 0 ≤ b) (hab : a + b = 1) (x y : X × Y),
  (Convexity.convexCombPair a b ha hb hab x y).2 = Convexity.convexCombPair a b ha hb hab x.2 y.2
-- Mathlib.Data.List.Lattice
List.forall_mem_inter_of_forall_right : ∀ {α : Type u_1} {l₂ : List α} {p : α → Prop} [inst : DecidableEq α] (l₁ : List α), (∀ x ∈ l₂, p x) → ∀ x ∈ l₁ ∩ l₂, p x
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.takeWhile_string_eq_takeWhile_toSlice : ∀ {pat : String} {s : String.Slice}, s.takeWhile pat = s.takeWhile pat.toSlice
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Use `mk` instead.  -/
Convexity.ConvexSpace.mk' : {R : Type u} →
  {M : Type v} →
    [inst₁ : PartialOrder R] →
      [inst₂ : Semiring R] →
        [inst₃ : IsStrictOrderedRing R] →
          (sConvexComb : Convexity.StdSimplex R M → M) →
            (∀ (x : M), sConvexComb (Convexity.StdSimplex.single x) = x) →
              (∀ (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)),
                  sConvexComb (Convexity.StdSimplex.map sConvexComb f) = sConvexComb f.join) →
                Convexity.ConvexSpace R M
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActionResult.closed.inj : ∀ {seq seq_1 : List Lean.Meta.Grind.TGrind},
  Lean.Meta.Grind.ActionResult.closed seq = Lean.Meta.Grind.ActionResult.closed seq_1 → seq = seq_1
-- Lean.Class
/-- Return `true` if `n` is the name of type class in the given environment.  -/
Lean.isClass : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- An arbitrarily chosen factorisation of a morphism out of a projective object through an epimorphism.
 -/
CategoryTheory.Projective.factorThru : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P X E : C} → [CategoryTheory.Projective P] → (P ⟶ X) → (e : E ⟶ X) → [CategoryTheory.Epi e] → P ⟶ E
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.toFun_eq_coe : ∀ {R : Type u_1} [inst : NonUnitalRing R] (p : RingNorm R), p.toFun = ⇑p
-- Mathlib.Data.ENat.Basic
instAddENat : Add ℕ∞
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R],
  ↑(Ideal.primeHeight✝ (IsLocalRing.maximalIdeal R)) = ringKrullDim R
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisors.associated_coe : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a b : ↥(nonZeroDivisors M₀)}, Associated ↑a ↑b ↔ Associated a b
-- Mathlib.Data.Finsupp.ToDFinsupp
Finsupp.toDFinsupp_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M], Finsupp.toDFinsupp 0 = 0
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_monomial_same : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) (a : R),
  (MvPowerSeries.coeff n) ((MvPowerSeries.monomial n) a) = a
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_eq_prod_of_inter_mulSupport_eq : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Set α} {t : Finset α},
  s ∩ Function.mulSupport f = ↑t ∩ Function.mulSupport f → ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- The weak kernel of a morphism.  -/
CategoryTheory.Limits.weakKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasWeakKernel f] → C
-- Mathlib.Control.Basic
Sum.instLawfulFunctor_mathlib : ∀ {e : Type v}, LawfulFunctor (Sum e)
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.CompletelyDistribLattice.MinimalAxioms.toCompleteDistribLattice.match_1_3.eq_2 : ∀ {α : Type u_1} (s : Set α)
  (motive :
    (i : ULift.{u_1, 0} Bool) →
      (match i with
        | { down := true } => PUnit.{u_1 + 1}
        | { down := false } => ↑s) →
        Sort u_2)
  (j :
    match { down := false } with
    | { down := true } => PUnit.{u_1 + 1}
    | { down := false } => ↑s)
  (h_1 :
    (j :
        match { down := true } with
        | { down := true } => PUnit.{u_1 + 1}
        | { down := false } => ↑s) →
      motive { down := true } j)
  (h_2 :
    (j :
        match { down := false } with
        | { down := true } => PUnit.{u_1 + 1}
        | { down := false } => ↑s) →
      motive { down := false } j),
  (match { down := false }, j with
    | { down := true }, j => h_1 j
    | { down := false }, j => h_2 j) =
    h_2 j
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_bijective : ∀ {R : Type u_1} {A : Type u_2}, Function.Bijective Unitization.toProd
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.isEmpty = true → m.getKey? a = none
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Localization.mulEquivOfQuotient_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (x : M) (y : ↥S), (Localization.mulEquivOfQuotient f) (Localization.mk x y) = f.mk' x y
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : Fintype ι]
  {β : ι → Type u_11} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i}
  [MeasureTheory.IsProbabilityMeasure μ],
  (∀ (i : ι), AEMeasurable (f i) μ) →
    (ProbabilityTheory.iIndepFun f μ ↔
      MeasureTheory.Measure.map (fun ω i => f i ω) μ =
        MeasureTheory.Measure.pi fun i => MeasureTheory.Measure.map (f i) μ)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.instFiniteDimensional : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [NumberField K] [NumberField L]
  [inst_4 : Algebra K L], FiniteDimensional K L
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Context.mk.injEq : ∀ (useMT : Bool) (thm : Lean.Meta.Grind.EMatchTheorem) (initApp : Lean.Expr) (useMT_1 : Bool)
  (thm_1 : Lean.Meta.Grind.EMatchTheorem) (initApp_1 : Lean.Expr),
  ({ useMT := useMT, thm := thm, initApp := initApp } = { useMT := useMT_1, thm := thm_1, initApp := initApp_1 }) =
    (useMT = useMT_1 ∧ thm = thm_1 ∧ initApp = initApp_1)
-- Lean.Server.FileWorker.SemanticHighlighting
/-- Start position of the semantic token.  -/
Lean.Server.FileWorker.AbsoluteLspSemanticToken.pos : Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Lsp.Position
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.lw : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {combined : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig combined → ℕ
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.State.mk.sizeOf_spec : ∀ (tokens : Lean.Parser.TokenTable) (kinds : Lean.Parser.SyntaxNodeKindSet) (categories : Lean.Parser.ParserCategories),
  sizeOf { tokens := tokens, kinds := kinds, categories := categories } =
    1 + sizeOf tokens + sizeOf kinds + sizeOf categories
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAtFilter.eq_1 : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (f : F → 𝕜) (f' x : F) (L : Filter F),
  HasGradientAtFilter f f' x L = HasFDerivAtFilter f ((InnerProductSpace.toDual 𝕜 F) f') (L ×ˢ pure x)
-- Mathlib.Algebra.Group.Defs
pow_right_comm : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), (a ^ m) ^ n = (a ^ n) ^ m
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.le_one : ∀ (x : ℝ), x.smoothTransition ≤ 1
-- Mathlib.Logic.Equiv.Defs
Equiv.right_inv : ∀ {α : Sort u_1} {β : Sort u_2} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- A chosen term in `FactorizationData W₁ W₂` when `HasFactorization W₁ W₂` holds.  -/
CategoryTheory.MorphismProperty.factorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W₁ W₂ : CategoryTheory.MorphismProperty C) → [W₁.HasFactorization W₂] → W₁.FactorizationData W₂
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- If `Γ` is a congruence subgroup, then so is `g⁻¹ Γ g ∩ SL(2, ℤ)` for any `g ∈ GL(2, ℚ)`.  -/
CongruenceSubgroup.IsCongruenceSubgroup.conjGL : ∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)},
  CongruenceSubgroup.IsCongruenceSubgroup Γ →
    ∀ (g : GL (Fin 2) ℚ),
      CongruenceSubgroup.IsCongruenceSubgroup
        (CongruenceSubgroup.conjGL Γ ((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ)) g))
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_comp : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (x : A), (Polynomial.aeval x) (p.comp q) = (Polynomial.aeval ((Polynomial.aeval x) q)) p
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache.core : Lean.Meta.LazyDiscrTree.Cache → Lean.Core.Cache
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.self_sub_monomial_natDegree_leadingCoeff : ∀ {R : Type u_2} [inst : Ring R] (f : Polynomial R), f - (Polynomial.monomial f.natDegree) f.leadingCoeff = f.eraseLead
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_sub_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s₁ s₂ t : Finset α}, s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.IsLocallyArtinian.of_locallyQuasiFinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.IsLocallyArtinian Y], AlgebraicGeometry.IsLocallyArtinian X
-- Mathlib.Algebra.Group.Action.Defs
vadd_add_vadd_comm : ∀ {α : Type u_5} {β : Type u_6} [inst : Add α] [inst_1 : Add β] [inst_2 : VAdd α β] [VAddAssocClass α β β]
  [VAddAssocClass α α β] [VAddCommClass α β β] (a : α) (b : β) (c : α) (d : β), (a +ᵥ b) + (c +ᵥ d) = (a + c) +ᵥ b + d
-- Mathlib.LinearAlgebra.Ray
/-- Negating a nonzero vector commutes with coercion to the underlying module.  -/
RayVector.coe_neg : ∀ {M : Type u_2} [inst : AddCommGroup M] {R : Type u_4} (v : RayVector R M),
  ↑((RayVector.equiv R M) (-v)) = -↑((RayVector.equiv R M) v)
-- Mathlib.Order.Directed
directed_comp_iff_of_surjective : ∀ {α : Type u_1} {ι : Sort u_3} {κ : Sort u_4} {r : α → α → Prop} {f : ι → κ},
  Function.Surjective f → ∀ {g : κ → α}, Directed r (g ∘ f) ↔ Directed r g
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_eq_iff_eq' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S}, f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f (x₁ * ↑y₂) = f (x₂ * ↑y₁)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumComm_inl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (n : WithTop ℕ∞) (M' : Type u_13)
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'], ⇑(Diffeomorph.sumComm I M n M') ∘ Sum.inl = Sum.inr
-- Mathlib.Data.Finset.Defs
Finset.lt_iff_ssubset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ⊂ s₂ ↔ s₁ ⊂ s₂
-- Std.Internal.Parsec.ByteArray
/-- Skip a `Char` that can be represented in 1 byte. If `c` uses more than 1 byte it is truncated.
 -/
Std.Internal.Parsec.ByteArray.skipByteChar : Char → Std.Internal.Parsec.ByteArray.Parser Unit
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSlice : (α : Type u_1) → [Ord α] → Type u_1
-- Batteries.Util.ProofWanted
/-- Elaborator that errors when `❰…❱` is used outside a wanted-declaration command.  -/
elabWantedRef : Lean.Elab.Term.TermElab
-- Mathlib.Data.Analysis.Topology
Ctop.mem_nhds_toTopsp : ∀ {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) {s : Set α} {a : α}, s ∈ nhds a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.Q_obj_single_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ) (X : C),
  DerivedCategory.Q.obj ((HomologicalComplex.single C (ComplexShape.up ℤ) n).obj X) =
    (DerivedCategory.singleFunctor C n).obj X
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.isNilpotent_toEnd_of_mem_rootSpace : ∀ {L : Type u_2} [inst : LieRing L] (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] {K : Type u_4}
  [inst_3 : Field K] [CharZero K] [inst_5 : LieAlgebra K L] (H : LieSubalgebra K L) [inst_6 : LieRing.IsNilpotent ↥H]
  [inst_7 : Module K M] [inst_8 : LieModule K L M] [LieModule.IsTriangularizable K (↥H) M] [FiniteDimensional K M]
  {x : L} {χ : ↥H → K}, χ ≠ 0 → x ∈ LieAlgebra.rootSpace H χ → IsNilpotent ((LieModule.toEnd K L M) x)
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.injective_iff_iterate_factorial_card_eq_id : ∀ {α : Type u_1} {f : α → α} [inst : Fintype α], Function.Injective f ↔ f^[(Fintype.card α).factorial] = id
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.mem_sup_left : ∀ {R : Type u} [inst : Semiring R] {S T : Ideal R} {x : R}, x ∈ S → x ∈ S ⊔ T
-- Mathlib.CategoryTheory.Functor.Currying
/-- The functor `uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E` is fully faithful.  -/
CategoryTheory.Functor.fullyFaithfulUncurry : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} → [inst_2 : CategoryTheory.Category.{v₄, u₄} E] → CategoryTheory.Functor.uncurry.FullyFaithful
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- `F.effectiveEpiOverObj X` provides an arbitrarily chosen object in the image of `F` equipped with an
effective epimorphism `F.effectiveEpiOver : F.effectiveEpiOverObj X ⟶ X`.
 -/
CategoryTheory.Functor.effectiveEpiOverObj : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → (F : CategoryTheory.Functor C D) → [F.EffectivelyEnough] → D → D
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.comp_iff : ∀ {T : Type u_3} [inst : CommRing T] {R : Type u_4} {S : Type u_5} [inst_1 : CommRing R] [inst_2 : CommRing S]
  {f : S →+* T} {g : R →+* S}, g.QuasiFinite → ((f.comp g).QuasiFinite ↔ f.QuasiFinite)
-- Init.Data.Vector.Lex
Vector.ltIrrefl : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2], Std.Irrefl fun x1 x2 => x1 < x2
-- Mathlib.GroupTheory.Congruence.Basic
/-- Given types with additions `M, N`, the product of two congruence relations
`c` on `M` and `d` on `N`: `(x₁, x₂), (y₁, y₂) ∈ M × N` are related by `c.prod d` iff `x₁`
is related to `y₁` by `c` and `x₂` is related to `y₂` by `d`.  -/
AddCon.prod : {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → AddCon M → AddCon N → AddCon (M × N)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_iff_map_conj_eq : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal ↔ ∀ (g : G), Subgroup.map (↑(MulAut.conj g)) H = H
-- Mathlib.Topology.Connected.LocallyPathConnected
connectedComponent_eq_iff_joined : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] (x y : X),
  connectedComponent x = connectedComponent y ↔ Joined x y
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
ofMul_list_prod : ∀ {M : Type u_3} [inst : Monoid M] (s : List M), Additive.ofMul s.prod = (List.map (⇑Additive.ofMul) s).sum
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The identity edge has an inverse.  -/
SSet.Edge.InvStruct.invStructId : {X : SSet} → (x : X.obj (Opposite.op { len := 0 })) → (SSet.Edge.id x).InvStruct
-- Mathlib.Data.Matrix.Mul
Matrix.op_smul_eq_mul_diagonal : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  [inst_2 : DecidableEq n] (M : Matrix m n α) (a : α), MulOpposite.op a • M = M * Matrix.diagonal fun x => a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Complex.sin` is complex analytic.  -/
Complex.analyticOn_sin : ∀ {s : Set ℂ}, AnalyticOn ℂ Complex.sin s
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ici_mul_Ici_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : DecidableEq α] [MulLeftMono α] [MulRightMono α]
  [inst_5 : LocallyFiniteOrderTop α] (a b : α), Finset.Ici a * Finset.Ici b ⊆ Finset.Ici (a * b)
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.NoRepetition.left_of_append : ∀ {α : Type u} {a : α} {l m : List α}, NoRepetition✝ a (l ++ m) → NoRepetition✝ a l
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.exists : ∀ {p : Complex.UnitDisc → Prop}, (∃ z, p z) ↔ ∃ z, ∃ (hz : ‖z‖ < 1), p (Complex.UnitDisc.mk z hz)
-- Mathlib.Order.Monotone.Basic
StrictAnti.injective : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → Function.Injective f
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_inj`. -/
Set.setOf_inj : ∀ {α : Type u} {p q : α → Prop}, {x | p x} = {x | q x} ↔ p = q
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.instPreadditive : {R : Type} → [inst : Ring R] → CategoryTheory.Preadditive (CategoryTheory.Mat R)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddTorsionFree : ∀ {α : Type u_1} [inst : AddMonoid α] [IsAddTorsionFree α], IsAddTorsionFree αᵃᵒᵖ
-- Mathlib.GroupTheory.Rank
Subgroup.nat_card_centralizer_nat_card_stabilizer : ∀ {G : Type u_1} [inst : Group G] (g : G),
  Nat.card ↥(Subgroup.centralizer {g}) = Nat.card ↥(MulAction.stabilizer (ConjAct G) g)