mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.Flat f]
  [AlgebraicGeometry.QuasiCompact f], (CategoryTheory.Over.pullback f).Faithful
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.memℓp : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)),
  Memℓp (↑f) p
-- Init.Data.String.Lemmas.FindPos
String.pos_eq_posLE : ∀ {s : String} {p : String.Pos.Raw} {h : String.Pos.Raw.IsValid s p}, s.pos p h = s.posLE p
-- Mathlib.Tactic.DuplicateDecls
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.instInhabitedModuleKey : Inhabited Mathlib.Tactic.DuplicateDecls.ModuleKey✝
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.ker_subgroupMap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) (f : G →* N),
  (f.subgroupMap H).ker = f.ker.subgroupOf H
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurable : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [SecondCountableTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ), Measurable τ
-- Init.MetaTypes
Lean.Meta.DSimp.Config.mk.inj : ∀ {zeta beta eta : Bool} {etaStruct : Lean.Meta.EtaStructMode}
  {iota proj decide autoUnfold failIfUnchanged unfoldPartialApp zetaDelta index zetaUnused zetaHave locals instances
    zeta_1 beta_1 eta_1 : Bool}
  {etaStruct_1 : Lean.Meta.EtaStructMode}
  {iota_1 proj_1 decide_1 autoUnfold_1 failIfUnchanged_1 unfoldPartialApp_1 zetaDelta_1 index_1 zetaUnused_1 zetaHave_1
    locals_1 instances_1 : Bool},
  { zeta := zeta, beta := beta, eta := eta, etaStruct := etaStruct, iota := iota, proj := proj, decide := decide,
        autoUnfold := autoUnfold, failIfUnchanged := failIfUnchanged, unfoldPartialApp := unfoldPartialApp,
        zetaDelta := zetaDelta, index := index, zetaUnused := zetaUnused, zetaHave := zetaHave, locals := locals,
        instances := instances } =
      { zeta := zeta_1, beta := beta_1, eta := eta_1, etaStruct := etaStruct_1, iota := iota_1, proj := proj_1,
        decide := decide_1, autoUnfold := autoUnfold_1, failIfUnchanged := failIfUnchanged_1,
        unfoldPartialApp := unfoldPartialApp_1, zetaDelta := zetaDelta_1, index := index_1, zetaUnused := zetaUnused_1,
        zetaHave := zetaHave_1, locals := locals_1, instances := instances_1 } →
    zeta = zeta_1 ∧
      beta = beta_1 ∧
        eta = eta_1 ∧
          etaStruct = etaStruct_1 ∧
            iota = iota_1 ∧
              proj = proj_1 ∧
                decide = decide_1 ∧
                  autoUnfold = autoUnfold_1 ∧
                    failIfUnchanged = failIfUnchanged_1 ∧
                      unfoldPartialApp = unfoldPartialApp_1 ∧
                        zetaDelta = zetaDelta_1 ∧
                          index = index_1 ∧
                            zetaUnused = zetaUnused_1 ∧
                              zetaHave = zetaHave_1 ∧ locals = locals_1 ∧ instances = instances_1
-- Mathlib.Order.Interval.Basic
NonemptyInterval.pure_injective : ∀ {α : Type u_1} [inst : Preorder α], Function.Injective NonemptyInterval.pure
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- If a function is `r`-Hölder over a bounded set,
then it is also `s`-Hölder over this set when `s ≤ r`. See `HolderOnWith.exists_holderOnWith_of_le`
for the version in a pseudometric space.  -/
HolderOnWith.exists_holderOnWith_of_le' : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {D s : NNReal} {A : Set X},
  (∃ C, HolderOnWith C r f A) →
    s ≤ r → (∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ ↑D) → ∃ C, HolderOnWith C s f A
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.forget_ε : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Mon.forget C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Lean.Meta.Tactic.Grind.Core
/-- Internalizes `lhs` and `rhs`, and then adds equality `lhs = rhs`.  -/
Lean.Meta.Grind.addNewEq : Lean.Expr → Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.det_eq_sign_charpoly_coeff : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.det = (-1) ^ Fintype.card n * M.charpoly.coeff 0
-- Mathlib.Topology.Connected.Clopen
/-- A set `s` is preconnected if and only if for every cover by two open sets that are disjoint on
`s`, it is contained in one of the two covering sets.  -/
isPreconnected_iff_subset_of_disjoint : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsPreconnected s ↔ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
-- Mathlib.CategoryTheory.Monoidal.Center
/-- A half-braiding on `X : C` is a family of isomorphisms `X ⊗ U ≅ U ⊗ X`,
monoidally natural in `U : C`.

Thinking of `C` as a 2-category with a single `0`-morphism, these are the same as natural
transformations (in the pseudo- sense) of the identity 2-functor on `C`, which send the unique
`0`-morphism to `X`.
 -/
CategoryTheory.HalfBraiding : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → Type (max u₁ v₁)
-- Mathlib.RingTheory.RingHomProperties
RingHom.RespectsIso.isLocalization_away_iff : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    ∀ {R S : Type u} (R' S' : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing R']
      [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] (f : R →+* S) (r : R)
      [inst_6 : IsLocalization.Away r R'] [inst_7 : IsLocalization.Away (f r) S'],
      P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- The characteristic function of a finite-measure measurable set `s`, as an `Lp` simple function.
 -/
MeasureTheory.Lp.simpleFunc.indicatorConst : {α : Type u_1} →
  {E : Type u_4} →
    [inst : MeasurableSpace α] →
      [inst_1 : NormedAddCommGroup E] →
        (p : ENNReal) →
          {μ : MeasureTheory.Measure α} →
            {s : Set α} → MeasurableSet s → μ s ≠ ⊤ → E → ↥(MeasureTheory.Lp.simpleFunc E p μ)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.instBraidedCategoryOpposite : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory Cᵒᵖ
-- Std.Do.SPred.SPred
Std.Do.SPred.bientails_cons_intro : ∀ {σs : List (Type u)} {σ : Type u} {P Q : Std.Do.SPred (σ :: σs)}, (∀ (s : σ), P s ⊣⊢ₛ Q s) → P ⊣⊢ₛ Q
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_union_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t₁ t₂ : Finset α), s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂)
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.le_iff' : ∀ {X : Type u_1} {d₁ d₂ : DiffeologicalSpace X},
  d₁ ≤ d₂ ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), Diffeology.IsPlot p → Diffeology.IsPlot p
-- Mathlib.Analysis.Normed.Module.Convex
Convex.cthickening : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s → ∀ (δ : ℝ), Convex ℝ (Metric.cthickening δ s)
-- Mathlib.Topology.Algebra.ConstMulAction
properlyDiscontinuousSMul_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α],
  ProperlyDiscontinuousSMul M α ↔ ∀ {K L : Set α}, IsCompact K → IsCompact L → {m | (m • K ∩ L).Nonempty}.Finite
-- Mathlib.Topology.Semicontinuity.Basic
IsClosed.upperSemicontinuousWithinAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s t : Set α} {x : α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsClosed s → 0 ≤ y → UpperSemicontinuousWithinAt (s.indicator fun _x => y) t x
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_nsmul' : ∀ {G : Type u_1} [inst : AddMonoid G] (x : G) {n : ℕ}, n ≠ 0 → addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n
-- Mathlib.CategoryTheory.Countable
/-- A countable category `α` is equivalent to a category with objects in `Type`.  -/
CategoryTheory.CountableCategory.ObjAsType : (α : Type u) → [inst : CategoryTheory.Category.{v, u} α] → [CategoryTheory.CountableCategory α] → Type
-- Mathlib.Order.Minimal
/-- If `P` is up-closed, then maximal elements satisfying `P` are exactly the globally maximal
elements satisfying `P`.  -/
maximal_iff_isMax : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α], (∀ ⦃x y : α⦄, P y → y ≤ x → P x) → (Maximal P x ↔ P x ∧ IsMax x)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.mul_smul' : ∀ (g h : GL (Fin 2) ℝ) (z : UpperHalfPlane),
  UpperHalfPlane.smulAux (g * h) z = UpperHalfPlane.smulAux g (UpperHalfPlane.smulAux h z)
-- Init.Data.Ord.Basic
Ordering.gt_beq_eq : (Ordering.gt == Ordering.eq) = false
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.norm_qParam_lt_iff : ∀ {h : ℝ}, 0 < h → ∀ (A : ℝ) (z : ℂ), ‖Function.Periodic.qParam h z‖ < Real.exp (-2 * Real.pi * A / h) ↔ A < z.im
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instMulAction : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {K : Type u_5} → [inst_1 : Monoid K] → [MulAction K β] → MulAction K (MeasureTheory.SimpleFunc α β)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ →
    Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.iff_transcendental_adjoin_image : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (i : ι),
  AlgebraicIndependent R x ↔
    (AlgebraicIndependent R fun j => x ↑j) ∧ Transcendental (↥(Algebra.adjoin R (x '' {i}ᶜ))) (x i)
-- Mathlib.Algebra.GroupWithZero.Associated
/-- Notation for two elements of a monoid being associated, i.e.
if one of them is another one multiplied by a unit on the right.  -/
_private.Mathlib.Algebra.GroupWithZero.Associated.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.span_isGroupLikeElem : ∀ {R : Type u_1} {A : Type u_3} {G : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  Submodule.span A {a | IsGroupLikeElem R a} = ⊤
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.mk_right_as : ∀ {S : AlgebraicGeometry.Scheme} {R : CommRingCat} (f : AlgebraicGeometry.Spec R ⟶ S)
  [inst : AlgebraicGeometry.Etale f], (AlgebraicGeometry.Scheme.AffineEtale.mk f).right.as = PUnit.unit
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.ofPostconditionT.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : Std.Iterators.PostconditionT m α),
  Std.Iterators.HetT.ofPostconditionT x =
    { Property := x.Property, small := ⋯, operation := Std.Internal.USquash.deflate <$> x.operation }
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.card_support_eq_two : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R},
  f.support.card = 2 ↔
    ∃ k m,
      ∃ (_ : k < m),
        ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.associator_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F G H : CategoryTheory.Functor C D} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.associator F G H).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (G.obj X) (H.obj X)).inv
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhds_coe_coe : ∀ {r p : ℝ}, nhds (↑r, ↑p) = Filter.map (fun p => (↑p.1, ↑p.2)) (nhds (r, p))
-- Mathlib.RingTheory.HopkinsLevitzki
IsSemiprimaryRing.isNoetherianRing_iff_jacobson_fg : ∀ {R : Type u_2} [inst : Ring R] [IsSemiprimaryRing R], IsNoetherianRing R ↔ (Ring.jacobson R).FG
-- Mathlib.Tactic.Linter.MinImports
/-- `ImportState` is the structure keeping track of the data that the `minImports` linter uses.
* `transClosure` is the import graph of the current file.
* `minImports` is the `NameSet` of minimal imports to build the file up to the current command.
* `importSize` is the number of transitive imports to build the file up to the current command.
 -/
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.ImportState : Type
-- Mathlib.Topology.UniformSpace.Basic
uniformity_subtype : ∀ {α : Type ua} {p : α → Prop} [inst : UniformSpace α],
  uniformity (Subtype p) = Filter.comap (fun q => (↑q.1, ↑q.2)) (uniformity α)
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunBilinear_apply_eq_sum : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R),
  ((PolyEquivTensor.toFunBilinear R A) a) p = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
-- Init.Data.UInt.Bitwise
UInt16.toUInt8_xor : ∀ (a b : UInt16), (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.add_of_omega0_opow_le`. -/
Ordinal.add_absorp : ∀ {a b c : Ordinal.{u}}, a < Ordinal.omega0 ^ b → Ordinal.omega0 ^ b ≤ c → a + c = c
-- Mathlib.Tactic.Constructor
/-- `econstructor`, on a goal which is an inductive type, solves it by applying the first matching
constructor, creating new goals for non-dependent arguments to the constructor in the same order.
This is like `constructor` except only non-dependent arguments are shown as new goals.
 -/
tacticEconstructor : Lean.ParserDescr
-- Mathlib.CategoryTheory.Products.Basic
/-- The Cartesian product functor between functor categories  -/
CategoryTheory.prodFunctor : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                CategoryTheory.Functor (CategoryTheory.Functor A B × CategoryTheory.Functor C D)
                  (CategoryTheory.Functor (A × C) (B × D))
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.elabConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Tactic.RingNF.Config
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.range_familyOfBFamily' : ∀ {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o)
  (f : (a : Ordinal.{u}) → a < o → α), Set.range (Ordinal.familyOfBFamily' r ho f) = o.brange f
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
FiniteDimensional.trans : ∀ (F : Type u_1) (K : Type u_2) (A : Type u_3) [inst : DivisionRing F] [inst_1 : DivisionRing K]
  [inst_2 : AddCommGroup A] [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A]
  [FiniteDimensional F K] [FiniteDimensional K A], FiniteDimensional F A
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_le_eq`. -/
setOf_gauge_le_eq : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {a : ℝ},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → 0 ≤ a → {x | gauge s x ≤ a} = ⋂ r, ⋂ (_ : a < r), r • s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = false → Std.DTreeMap.Const.get? t a = none
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTransposeAddEquiv_apply : ∀ (m : Type u_2) (n : Type u_3) (α : Type v) [inst : AddMonoid α] [inst_1 : StarAddMonoid α] (M : Matrix m n α),
  (Matrix.conjTransposeAddEquiv m n α) M = M.conjTranspose
-- Mathlib.LinearAlgebra.Matrix.Basis
basis_toMatrix_mul_linearMap_toMatrix : ∀ {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  (b' : Module.Basis ι' R M) (c : Module.Basis κ R N) (c' : Module.Basis κ' R N) (f : M →ₗ[R] N) [inst_5 : Fintype ι']
  [inst_6 : Finite κ] [inst_7 : Fintype κ'] [inst_8 : DecidableEq ι'],
  c.toMatrix ⇑c' * (LinearMap.toMatrix b' c') f = (LinearMap.toMatrix b' c) f
-- Batteries.Recycling.RBTree.Basic
/-- `insert cmp t v` inserts element `v` into the tree, using the provided comparator
`cmp` to put it in the right place and automatically rebalancing the tree as necessary.
 -/
RBTree.RBNode.insert : {α : Type u_1} → (α → α → Ordering) → RBTree.RBNode α → α → RBTree.RBNode α
-- Mathlib.RingTheory.PowerBasis
PowerBasis.exists_eq_aeval' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (pb : PowerBasis R S)
  (y : S), ∃ f, y = (Polynomial.aeval pb.gen) f
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.alts.injEq : ∀ (ref : Lean.Syntax) (a : List Lean.Elab.Tactic.RCases.RCasesPatt) (ref_1 : Lean.Syntax)
  (a_1 : List Lean.Elab.Tactic.RCases.RCasesPatt),
  (Lean.Elab.Tactic.RCases.RCasesPatt.alts ref a = Lean.Elab.Tactic.RCases.RCasesPatt.alts ref_1 a_1) =
    (ref = ref_1 ∧ a = a_1)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.mul_div_one : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {p r : R} {s : ↥S},
  p /ₒ s * (r /ₒ 1) = p * r /ₒ s
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- **Divergence theorem** for Bochner integral. If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is continuous on a rectangular
box `[a, b] : Set ℝⁿ⁺¹`, `a ≤ b`, is differentiable on its interior with derivative
`f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹` and the divergence `fun x ↦ ∑ i, f' x eᵢ i` is integrable on `[a, b]`,
where `eᵢ = Pi.single i 1` is the `i`-th basis vector, then its integral is equal to the sum of
integrals of `f` over the faces of `[a, b]`, taken with appropriate signs.

Moreover, the same is true if the function is not differentiable at countably many
points of the interior of `[a, b]`.

We represent both faces `x i = a i` and `x i = b i` as the box
`face i = [a ∘ Fin.succAbove i, b ∘ Fin.succAbove i]` in `ℝⁿ`, where
`Fin.succAbove : Fin n ↪o Fin (n + 1)` is the order embedding with range `{i}ᶜ`. The restrictions
of `f : ℝⁿ⁺¹ → Eⁿ⁺¹` to these faces are given by `f ∘ backFace i` and `f ∘ frontFace i`, where
`backFace i = Fin.insertNth i (a i)` and `frontFace i = Fin.insertNth i (b i)` are embeddings
`ℝⁿ → ℝⁿ⁺¹` that take `y : ℝⁿ` and insert `a i` (resp., `b i`) as `i`-th coordinate.  -/
MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} (a b : Fin (n + 1) → ℝ),
  a ≤ b →
    ∀ (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E)
      (s : Set (Fin (n + 1) → ℝ)),
      s.Countable →
        ContinuousOn f (Set.Icc a b) →
          (∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x) →
            MeasureTheory.IntegrableOn (fun x => ∑ i, (f' x) (Pi.single i 1) i) (Set.Icc a b) MeasureTheory.volume →
              ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (Pi.single i 1) i =
                ∑ i,
                  ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
                    ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.hasForgetToAddCommGrp : CategoryTheory.HasForget₂ RingCat AddCommGrpCat
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The equalizer of morphisms `f g : X ⟶ Y` as a `Subobject X`.  -/
CategoryTheory.Limits.equalizerSubobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f g : X ⟶ Y) → [CategoryTheory.Limits.HasEqualizer f g] → CategoryTheory.Subobject X
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If a functor `G` has the same collection of cones as a functor `F`
which has a limit, then `G` also has a limit.  -/
CategoryTheory.Limits.HasLimit.ofConesIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J K : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  [inst_2 : CategoryTheory.Category.{v₂, u₁} K] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor K C)
  (h : F.cones ≅ G.cones) [CategoryTheory.Limits.HasLimit F], CategoryTheory.Limits.HasLimit G
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.RightLinear C] (d : D) (c : C) {Z : D'}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) h) =
    h
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) {x : α},
  ↑(e.trans e') x = ↑e' (↑e x)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.mk.injEq : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (toAddMonoidHom : G →+ E)
  (rightInverse_rightHom : Function.RightInverse (↑toAddMonoidHom).toFun ⇑S.rightHom) (toAddMonoidHom_1 : G →+ E)
  (rightInverse_rightHom_1 : Function.RightInverse (↑toAddMonoidHom_1).toFun ⇑S.rightHom),
  ({ toAddMonoidHom := toAddMonoidHom, rightInverse_rightHom := rightInverse_rightHom } =
      { toAddMonoidHom := toAddMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 }) =
    (toAddMonoidHom = toAddMonoidHom_1)
-- Init.Data.List.Impl
List.eraseIdx.eq_def : ∀ {α : Type u} (x : List α) (x_1 : ℕ),
  x.eraseIdx x_1 =
    match x, x_1 with
    | [], x => []
    | head :: as, 0 => as
    | a :: as, n.succ => a :: as.eraseIdx n
-- Mathlib.Algebra.Lie.AdjointAction.Basic
LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_3} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (K : LieSubalgebra R L) {x : ↥K}, IsNilpotent ((LieAlgebra.ad R L) ↑x) → IsNilpotent ((LieAlgebra.ad R ↥K) x)
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.binomial_eq_choose : ∀ {α : Type u_1} {f : α → ℕ} {a b : α} [inst : DecidableEq α],
  a ≠ b → Nat.multinomial {a, b} f = (f a + f b).choose (f a)