mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotent_of_mulEquiv`.

---

Nilpotency respects isomorphisms.  -/
nilpotent_of_mulEquiv : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] [_h : Group.IsNilpotent G] (f : G ≃* G'),
  Group.IsNilpotent G'
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∃ t ⊆ s, MeasurableSet t ∧ t =ᵐ[μ] s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂).get? k = t₁.get? k
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_le_iff : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ k, p k) (i : Fin n), Fin.find p h ≤ i ↔ ∃ m ≤ i, p m
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_compl : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Closeds α), ↑s.compl = (↑s)ᶜ
-- Lean.Elab.MutualInductive
/-- Descriptor for a command processor that elaborates an inductive type.

Elaboration occurs in the following steps:
- Every command has its `mkInductiveView` evaluated, producing `InductiveView`s and callbacks
  for the next steps (all recorded in `InductiveElabStep1`).
- Each `InductiveView` gets elaborated, creating `ElabHeaderResult`s, and the local contexts are unified into a single one
  with a consistent set of parameters between each inductive.
- Each callback is called to elaborate each inductives' constructors and some additional callbacks
  (all recorded in `InductiveElabStep2`).
- Fvars are collected from the constructors and from the `InductiveStep2.collectUsedFVars` callbacks.
  This is used to compute the final set of scoped variables that should be used as additional parameters.
- Universe levels are checked. Commands can give custom errors using `InductiveStep2.checkUniverses`.
- Elaboration of constructors is finalized, with additional tasks done by each `InductiveStep2.finalizeTermElab`.
- The inductive family is added to the environment and is checked by the kernel.
- Attributes and other finalization activities are performed, including those defined
  by `InductiveStep2.prefinalize` and `InductiveStep3.finalize`.
 -/
Lean.Elab.Command.InductiveElabDescr : Type
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView!.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.maxView! k v l Std.DTreeMap.Internal.Impl.leaf = { k := k, v := v, tree := l }
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isIso_whiskerRight : ∀ {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] {G H : CategoryTheory.Functor C D} (α : G ⟶ H)
  (F : CategoryTheory.Functor D E) [CategoryTheory.IsIso α],
  CategoryTheory.IsIso (CategoryTheory.Functor.whiskerRight α F)
-- Std.Sat.AIG.CNF
/-- A cache with no entries is valid for an empty CNF.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.init : (aig : Std.Sat.AIG ℕ) → Std.Sat.AIG.toCNF.Cache✝ aig Std.Sat.CNF.empty
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_smul : ∀ {α : Type u_1} {R : Type u_2} [inst : SMul R α] (c : R) (a : αˢʸᵐ), SymAlg.unsym (c • a) = c • SymAlg.unsym a
-- Mathlib.LinearAlgebra.InvariantBasisNumber
card_le_of_injective : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {α : Type u_1} {β : Type u_2} [inst_2 : Fintype α]
  [inst_3 : Fintype β] (f : (α → R) →ₗ[R] β → R), Function.Injective ⇑f → Fintype.card α ≤ Fintype.card β
-- Mathlib.LinearAlgebra.Dimension.Constructions
subalgebra_top_finrank_eq_submodule_top_finrank : ∀ {F : Type u_2} {E : Type u_3} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E],
  Module.finrank F ↥⊤ = Module.finrank F ↥⊤
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_antitone : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G), Antitone S.lowerCentralSeries
-- Mathlib.CategoryTheory.Action.Concrete
/-- If `N` and `H` are subgroups of a group `G` with `N ≤ H`, this is the canonical
`G`-morphism `G ⧸ N ⟶ G ⧸ H`.  -/
Action.FintypeCat.quotientToQuotientOfLE : {G : Type u_1} →
  [inst : Group G] →
    (H N : Subgroup G) →
      [inst_1 : Fintype (G ⧸ N)] →
        [inst_2 : Fintype (G ⧸ H)] →
          N ≤ H →
            (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)) ⟶
              Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ H)))
-- Mathlib.CategoryTheory.Action.Basic
Action.ρ_one : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] (A : Action V G),
  A.ρ 1 = CategoryTheory.CategoryStruct.id A.V
-- Init.Data.UInt.Lemmas
UInt64.ofNat_mod : ∀ {a b : ℕ}, a < 2 ^ 64 → b < 2 ^ 64 → UInt64.ofNat (a % b) = UInt64.ofNat a % UInt64.ofNat b
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise multiplication of `f` and `g`,
which antivary together, is unchanged by a permutation if and only if `f` and `g ∘ σ` antivary
together. Stated by permuting the entries of `g`.  -/
Antivary.sum_mul_eq_sum_mul_comp_perm_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι],
  Antivary f g → (∑ i, f i * g (σ i) = ∑ i, f i * g i ↔ Antivary f (g ∘ ⇑σ))
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.instMonadCommRingOfMonadLift : (m n : Type → Type) →
  [MonadLift m n] → [Lean.Meta.Grind.Arith.CommRing.MonadCommRing m] → Lean.Meta.Grind.Arith.CommRing.MonadCommRing n
-- Mathlib.Data.Set.MulAntidiagonal
Set.MulAntidiagonal.eq_of_snd_eq_snd : ∀ {α : Type u_1} [inst : CommMonoid α] [IsCancelMul α] {s t : Set α} {a : α} {x y : ↑(s.mulAntidiagonal t a)},
  (↑x).2 = (↑y).2 → x = y
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph1_le_mk : ∀ (α : Type u_1) [Uncountable α], Cardinal.aleph 1 ≤ Cardinal.mk α
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.domRestrict_eq_one_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {S : Type u_3}
  [inst_2 : SetLike S R] [inst_3 : SubmonoidClass S R] {T : S} {χ : MulChar R R'},
  MulChar.domRestrict T χ = 1 ↔ ∀ (x : (↥T)ˣ), χ ↑↑x = 1
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- A standard basis matrix is in $J(Mₙ(I))$
as long as its one possibly non-zero entry is in $J(I)$.  -/
Ideal.single_mem_jacobson_matrix : ∀ {R : Type u_1} [inst : Ring R] {n : Type u_2} [inst_1 : Fintype n] [inst_2 : DecidableEq n] (I : Ideal R),
  ∀ x ∈ I.jacobson, ∀ (i j : n), Matrix.single i j x ∈ (Ideal.matrix n I).jacobson
-- Mathlib.Algebra.Lie.Normalizer
LieSubalgebra.mem_normalizer_iff : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) (x : L), x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
-- Lean.Meta.Closure
Lean.Meta.Closure.mkLambda : Array Lean.LocalDecl → Lean.Expr → Lean.Expr
-- Lean.Data.Lsp.Diagnostics
/-- A data entry field that is preserved between a `textDocument/publishDiagnostics` notification and `textDocument/codeAction` request.  -/
Lean.Lsp.DiagnosticWith.data? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option Lean.Json
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidal_tensorUnit_as : ∀ (M : Type u) [inst : Monoid M], (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete M)).as = 1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.OpenCover.restrict_f : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (U : X.Opens) (x : 𝒰.I₀), (𝒰.restrict U).f x = 𝒰.f x ∣_ U
-- Mathlib.Order.SetDissipate
Set.dissipate_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] (s : α → Set β), Set.dissipate s ⊥ = s ⊥
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_neg_one : ∀ (L : List ℕ), Nat.ofDigits (-1) L = (List.map (fun n => ↑n) L).alternatingSum
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mker_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mker (Monoid.Coprod.swap M N) = ⊥
-- Mathlib.Order.ModularLattice
/-- `a ⊔ b` covers `a` and `b` if either `a` or `b` covers `a ⊓ b`  -/
IsUpperModularLattice.covBy_sup_of_inf_covBy : ∀ {α : Type u_2} {inst : Lattice α} [self : IsUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → b ⋖ a ⊔ b
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousAt.inf : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} {r' : α → β → Prop},
  SemicontinuousAt r x → SemicontinuousAt r' x → SemicontinuousAt (r ⊓ r') x
-- Init.Data.Array.OfFn
Array.ofFnM_zero : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] {f : Fin 0 → m α}, Array.ofFnM f = pure #[]
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.essSurj_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.EssSurj] [F₂.EssSurj] [F.Full] [CategoryTheory.IsIso α]
  [CategoryTheory.IsIso β], (CategoryTheory.Comma.map α β).EssSurj
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The additive monoid algebra over a semiring `R` generated by the additive monoid `M`.

It is the type of finite formal `R`-linear combinations of terms of `M`,
endowed with the convolution product.  -/
AddMonoidAlgebra.«term__[_]» : Lean.TrailingParserDescr
-- Mathlib.Data.Finset.Range
Finset.range_subset : ∀ {n : ℕ} {s : Finset ℕ}, Finset.range n ⊆ s ↔ ∀ x < n, x ∈ s
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_factors_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} (h : W ⟶ X),
  (CategoryTheory.Limits.equalizerSubobject f g).Factors h ↔
    CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
-- Mathlib.CategoryTheory.Limits.FullSubcategory
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (J : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} J] [CategoryTheory.Limits.HasLimitsOfShape J P.FullSubcategory]
  [P.IsClosedUnderIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfShape J P.ι], P.IsClosedUnderLimitsOfShape J
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.continuousAt_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T3Space γ] {b : β} {f : α → γ} (di : IsDenseInducing i),
  (∀ᶠ (x : β) in nhds b, ∃ c, Filter.Tendsto f (Filter.comap i (nhds x)) (nhds c)) → ContinuousAt (di.extend f) b
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNat.eq_def : ∀ (q x : ℕ),
  LucasLehmer.norm_num_ext.sModNat q x =
    match x with
    | 0 => 4 % q
    | i.succ => (LucasLehmer.norm_num_ext.sModNat q i ^ 2 + (q - 2)) % q
-- Mathlib.Data.Set.Operations
Set.instCompl : {α : Type u} → Compl (Set α)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Transport a term of type `IsInitial` across an isomorphism.  -/
CategoryTheory.Limits.IsInitial.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → CategoryTheory.Limits.IsInitial X → (X ≅ Y) → CategoryTheory.Limits.IsInitial Y
-- Mathlib.Order.UpperLower.Basic
isLowerSet_compl : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsLowerSet sᶜ ↔ IsUpperSet s
-- Init.Control.Lawful.Basic
/-- `seqLeft` is equivalent to the default implementation.  -/
LawfulApplicative.seqLeft_eq : ∀ {f : Type u → Type v} {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (x : f α) (y : f β),
  x <* y = Function.const β <$> x <*> y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.toArray_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.toArray = t₂.toArray
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.comp_hom'`. -/
CategoryTheory.Mod_.comp_hom' : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N K : CategoryTheory.Mod D A} (f : M ⟶ N) (g : N ⟶ K),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Topology.Order.OrderClosed
ge_of_tendsto_of_frequently : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {f : β → α}
  {a b : α} {x : Filter β}, Filter.Tendsto f x (nhds a) → (∃ᶠ (c : β) in x, b ≤ f c) → b ≤ a
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wpRec : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_2} n} →
      {C : Sort u_1} →
        ((a : P.A) → (f : P.last.B a → P.last.W) → TypeVec.Arrow (P.WPath (WType.mk a f)) α → (P.last.B a → C) → C) →
          (x : P.last.W) → TypeVec.Arrow (P.WPath x) α → C
-- Mathlib.Data.DFinsupp.Order
DFinsupp.single_nonneg : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)] {i : ι} {a : α i}
  [inst_2 : DecidableEq ι], (0 ≤ fun₀ | i => a) ↔ 0 ≤ a
-- Init.Data.List.BasicAux
List.getElem_append_right : ∀ {α : Type u_1} {as bs : List α} {i : ℕ} (h₁ : as.length ≤ i) {h₂ : i < (as ++ bs).length},
  (as ++ bs)[i] = bs[i - as.length]
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.completeness : Lean.Server.StatefulRequestHandler → Lean.Server.RequestHandlerCompleteness
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.Dual.isCompl_ker_of_disjoint_of_ne_bot : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  {f : Module.Dual K V₁},
  f ≠ 0 →
    ∀ [FiniteDimensional K V₁] {p : Submodule K V₁}, Disjoint (LinearMap.ker f) p → p ≠ ⊥ → IsCompl (LinearMap.ker f) p
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeFormAux_apply_apply : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (B : LinearMap.BilinForm R M) (a : M) (a_1 : CliffordAlgebra Q),
  ((CliffordAlgebra.changeFormAux Q B) a) a_1 = (CliffordAlgebra.ι Q) a * a_1 - (CliffordAlgebra.contractLeft (B a)) a_1
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.iff_preimage_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- The fudge factor that appears in the formula for the volume of `convexBodyLt`.  -/
NumberField.mixedEmbedding.convexBodySumFactor : (K : Type u_1) → [inst : Field K] → [NumberField K] → NNReal
-- Init.Data.Bool
Bool.rec_eq : ∀ {α : Sort u_1} (b : Bool) {x y : α}, Bool.rec y x b = if b = true then x else y
-- Mathlib.Data.Sum.Order
Sum.Lex.toLex_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], Monotone ⇑toLex
-- Mathlib.RingTheory.Polynomial.Vieta
MvPolynomial.prod_X_add_C_coeff : ∀ (R : Type u_1) (σ : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype σ],
  ∀ k ≤ Fintype.card σ,
    (∏ i, (Polynomial.X + Polynomial.C (MvPolynomial.X i))).coeff k = MvPolynomial.esymm σ R (Fintype.card σ - k)
-- Lean.DocString.Types
/-- Rewrites using proofs that inline element types, block types, and metadata types are equal.  -/
Lean.Doc.Part.cast : {i i' : Type u_1} →
  {b b' : Type u_2} → {p p' : Type u_3} → i = i' → b = b' → p = p' → Lean.Doc.Part i b p → Lean.Doc.Part i' b' p'
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.instIsEquivalenceOppositeLeftOp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} [F.IsEquivalence], F.leftOp.IsEquivalence
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `C^n` as continuity and being `C^n` in any extended chart.  -/
contMDiff_iff : ∀ {𝕜 : 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'] {f : M → M'} {n : WithTop ℕ∞}
  [IsManifold I n M] [IsManifold I' n M'],
  ContMDiff I I' n f ↔
    Continuous f ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' f ⁻¹' (extChartAt I' y).source)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- Conditional expectation commutes with continuous linear maps.  -/
ContinuousLinearMap.comp_condExp_comm : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {F : Type u_5}
  [inst_3 : NormedAddCommGroup F] [CompleteSpace F] [inst_5 : NormedSpace ℝ F],
  MeasureTheory.Integrable f μ → ∀ (T : E →L[ℝ] F), ⇑T ∘ μ[f | m] =ᵐ[μ] μ[⇑T ∘ f | m]
-- Mathlib.Algebra.Group.Basic
/-- Composing two additions on the right by `y` and `x`
is equal to an addition on the right by `y + x`.  -/
comp_add_right : ∀ {α : Type u_1} [inst : AddSemigroup α] (x y : α), ((fun x_1 => x_1 + x) ∘ fun x => x + y) = fun x_1 => x_1 + (y + x)
-- Mathlib.Order.Category.BddLat
/-- The category of bounded lattices with bounded lattice morphisms.  -/
BddLat : Type (u_1 + 1)
-- Mathlib.Analysis.Normed.Group.Uniform
SeminormedAddCommGroup.to_lipschitzAdd : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E], LipschitzAdd E
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (X : C) → [commRingObj : CategoryTheory.CommRingObj X] → CategoryTheory.CommRingObjCat C
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.add_comp : ∀ {E : Type u_3} {F : Type u_4} [inst : Group E] [inst_1 : Group F] (p q : GroupSeminorm E) (f : F →* E),
  (p + q).comp f = p.comp f + q.comp f
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal.mk.injEq : ∀ (mvarId : Lean.MVarId) (indicesFVarIds : Array Lean.FVarId) (fvarId : Lean.FVarId) (numEqs : ℕ)
  (mvarId_1 : Lean.MVarId) (indicesFVarIds_1 : Array Lean.FVarId) (fvarId_1 : Lean.FVarId) (numEqs_1 : ℕ),
  ({ mvarId := mvarId, indicesFVarIds := indicesFVarIds, fvarId := fvarId, numEqs := numEqs } =
      { mvarId := mvarId_1, indicesFVarIds := indicesFVarIds_1, fvarId := fvarId_1, numEqs := numEqs_1 }) =
    (mvarId = mvarId_1 ∧ indicesFVarIds = indicesFVarIds_1 ∧ fvarId = fvarId_1 ∧ numEqs = numEqs_1)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.map_fun : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Equiv M N)
  {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
/-- The Iwasawa structure on PSL(2, F).  -/
PSL2.Iwasawa : {F : Type u_2} →
  [inst : Field F] →
    MulAction.IwasawaStructure (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F) (Projectivization F (Fin 2 → F))
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_σ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 1)) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter_σ._auto_1),
  autoParam (↑j ≤ i) CategoryTheory.SimplicialObject.σ₀Iter_σ._auto_3 →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := m + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ₀Iter i hi) (CategoryTheory.CategoryStruct.comp (X.σ j) h) =
        CategoryTheory.CategoryStruct.comp (X.σ₀Iter (i + 1) ⋯) h
-- Mathlib.AlgebraicGeometry.Limits
/-- The images of each component in the coproduct is disjoint.  -/
AlgebraicGeometry.disjoint_opensRange_sigmaι : ∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ] (i j : σ),
  i ≠ j →
    Disjoint (AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι g i))
      (AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.Sigma.ι g j))
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.toAddEquiv_toNatLinearEquiv : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] (e : M ≃ₗ[ℕ] M₂),
  (↑e).toNatLinearEquiv = e
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_mul_inv_eq_convolution_inv : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  {ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x}.card = A.convolution B⁻¹ x
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd'_inv_app_f : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n₁ n₂ n₁₂ : ℤ)
  (h : n₁ + n₂ = n₁₂) (X : CochainComplex C ℤ) (i : ℤ),
  ((CochainComplex.shiftFunctorAdd' C n₁ n₂ n₁₂ h).inv.app X).f i = (HomologicalComplex.XIsoOfEq X ⋯).inv
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.zero_of_zero : ∀ {e : ONote} {n : ℕ+} {a : ONote}, (e.oadd n a).NF → e = 0 → a = 0
-- Std.Time.DateTime
Std.Time.DateTime.instHAddOffset_6 : HAdd Std.Time.DateTime Std.Time.Nanosecond.Offset Std.Time.DateTime
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemContKind.duplicable.sizeOf_spec : sizeOf Lean.Elab.Do.DoElemContKind.duplicable = 1
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.denom_S : ∀ (z : UpperHalfPlane),
  UpperHalfPlane.denom
      (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)) ↑z =
    ↑z
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *⋆-algebra* equivalence is an equivalence preserving addition, multiplication, scalar
multiplication and the star operation, which allows for considering both unital and non-unital
equivalences with a single structure.  -/
«term_≃⋆ₐ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- A version of `Complex.ofReal_exp` for `NormedSpace.exp` instead of `Complex.exp`  -/
NormedSpace.ofReal_exp_ℝ_ℝ : ∀ (r : ℝ), ↑(NormedSpace.exp r) = NormedSpace.exp ↑r