mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coalgebraEquivOver_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  (CategoryTheory.coalgebraEquivOver X).inverse = CategoryTheory.overToCoalgebra X
-- Mathlib.RingTheory.Ideal.Maps
RingHom.eq_liftOfRightInverse : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g)
  (h : B →+* C), h.comp f = g → h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩
-- Mathlib.Data.Analysis.Topology
Ctop.instCoeFunForallSet : {α : Type u_1} → {σ : Type u_3} → CoeFun (Ctop α σ) fun x => σ → Set α
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddMonoidHom.mk.congr_simp : ∀ {M : Type u_10} {N : Type u_11} [inst : AddZero M] [inst_1 : AddZero N] (toZeroHom toZeroHom_1 : ZeroHom M N)
  (e_toZeroHom : toZeroHom = toZeroHom_1)
  (map_add' : ∀ (x y : M), toZeroHom.toFun (x + y) = toZeroHom.toFun x + toZeroHom.toFun y),
  { toZeroHom := toZeroHom, map_add' := map_add' } = { toZeroHom := toZeroHom_1, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_η_ε_assoc : ∀ {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 D] {C' : Type u₁'}
  [inst_4 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal]
  (G : CategoryTheory.Functor D C') {Z : C'}
  (h : G.obj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.η F))
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.LaxMonoidal.ε F)) h) =
    h
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.CodescendsAlong.inf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q W : CategoryTheory.MorphismProperty C}
  [P.CodescendsAlong Q] [W.CodescendsAlong Q], (P ⊓ W).CodescendsAlong Q
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_mul : ∀ (R : Type u_1) {A : Type u_2} [inst : MulZeroClass R] [inst_1 : AddZeroClass A] [inst_2 : Mul A]
  [inst_3 : SMulWithZero R A] (a₁ a₂ : A), ↑(a₁ * a₂) = ↑a₁ * ↑a₂
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing.sizeOf_spec : ∀ (a b : Lean.Expr) (ra rb : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly)
  (lhs' : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreCommRing a b ra rb p lhs') =
    1 + sizeOf a + sizeOf b + sizeOf ra + sizeOf rb + sizeOf p + sizeOf lhs'
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The right homology in the opposite category of the opposite of a short complex identifies
to the left homology of this short complex.  -/
CategoryTheory.ShortComplex.rightHomologyOpIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasLeftHomology] → S.op.rightHomology ≅ Opposite.op S.leftHomology
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.finite : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] [Finite R], Finite S
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {t : Set X} {μ : MeasureTheory.Measure X}, (∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0) → ∫ (x : X) in t, f x ∂μ = 0
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_Y : ∀ {R : Type u_1} [inst : CommSemiring R], Polynomial.Bivariate.swap Polynomial.X = Polynomial.C Polynomial.X
-- Mathlib.Analysis.Analytic.Composition
/-- The `n`th coefficient of `id 𝕜 E` is the identity when `n = 1`. We state this in a dependent
way, as it will often appear in this form.  -/
FormalMultilinearSeries.id_apply_one' : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E) {n : ℕ} (h : n = 1) (v : Fin n → E),
  (FormalMultilinearSeries.id 𝕜 E x n) v = v ⟨0, ⋯⟩
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.realizeValue.unsafe_3 : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → NonScalar → Lean.PHashMap α (Task Dynamic)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarDecl.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (kind : Lean.Elab.Term.SyntheticMVarKind),
  sizeOf { stx := stx, kind := kind } = 1 + sizeOf stx + sizeOf kind
-- Mathlib.RingTheory.Length
Module.length_eq_one_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R M = 1 ↔ IsSimpleModule R M
-- Mathlib.Analysis.Real.Sqrt
NNReal.continuous_sqrt : Continuous ⇑NNReal.sqrt
-- Mathlib.Probability.Independence.InfinitePi
/-- Consider `((Xᵢⱼ)ⱼ)ᵢ` a family of families of random variables.
Assume that for any `i`, the random variables `(Xᵢⱼ)ⱼ` are independent.
Assume furthermore that the random variables `((Xᵢⱼ)ⱼ)ᵢ` are independent.
Then the random variables `(Xᵢⱼ)` indexed by pairs `(i, j)` are independent.

This is a dependent version of `iIndepFun_uncurry'`.  -/
ProbabilityTheory.iIndepFun_uncurry : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {κ : ι → Type u_4}
  {𝓧 : (i : ι) → κ i → Type u_5} {m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)}
  {X : (i : ι) → (j : κ i) → Ω → 𝓧 i j},
  (∀ (i : ι) (j : κ i), Measurable (X i j)) →
    ProbabilityTheory.iIndepFun (fun i ω x => X i x ω) P →
      (∀ (i : ι), ProbabilityTheory.iIndepFun (X i) P) → ProbabilityTheory.iIndepFun (fun p ω => X p.fst p.snd ω) P
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsColimit.reflects : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsColimit K F]
  {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit (F.mapCocone c)),
  Nonempty (CategoryTheory.Limits.IsColimit c)
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.add_mem : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) {x y : L}, x ∈ L' → y ∈ L' → x + y ∈ L'
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.swap_obj_inr : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : D), (CategoryTheory.Sum.swap C D).obj (Sum.inr X) = Sum.inl X
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.mem_iff_eq_smul_generator : ∀ {R : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] (S : Submodule R M)
  [inst_3 : S.IsPrincipal] {x : M}, x ∈ S ↔ ∃ s, x = s • Submodule.IsPrincipal.generator S
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_comp : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] (e : Module.Basis ι A M) (f : M →ₗ[A] M) (v : ι → M),
  e.det (⇑f ∘ v) = LinearMap.det f * e.det v
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.const_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → ∀ (c : F), DiffContOnCl 𝕜 (fun x => c + f x) s
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} [inst : Std.OrientedCmp cmp] {t : RBTree.RBNode α},
  (RBTree.RBNode.insert cmp t x).reverse = RBTree.RBNode.insert (flip cmp) t.reverse x
-- Mathlib.Topology.Instances.Int
/-- **Alias** of `IsOrderBornology.cobounded_eq`. -/
Int.cobounded_eq : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : LinearOrder α] [IsOrderBornology α] [NoMaxOrder α] [NoMinOrder α],
  Bornology.cobounded α = Filter.atBot ⊔ Filter.atTop
-- Mathlib.Topology.MetricSpace.Dilation
/-- The ratio of a dilation `f`. If the ratio is undefined (i.e., the distance between any two
points in `α` is either zero or infinity), then we choose one as the ratio.  -/
Dilation.ratio : {α : Type u_1} →
  {β : Type u_2} →
    {F : Type u_4} →
      [inst : PseudoEMetricSpace α] →
        [inst_1 : PseudoEMetricSpace β] → [inst_2 : FunLike F α β] → [DilationClass F α β] → F → NNReal
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.continuousOn_Ici : ∀ {f : ℝ → ℝ} {y : ℝ}, ConcaveOn ℝ (Set.Ici y) f → ContinuousWithinAt f (Set.Ici y) y → ContinuousOn f (Set.Ici y)
-- Lean.PrettyPrinter.Formatter
/-- Whether the resulting format must be grouped when used in a category formatter.
If the flag is set to false, then categoryParser omits the fill+nest operation.  -/
Lean.PrettyPrinter.Formatter.State.mustBeGrouped : Lean.PrettyPrinter.Formatter.State → Bool
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instRepr : {α : Type u} → {β : Type v} → [Repr α] → [Repr β] → Repr (Std.HashMap.Raw α β)
-- Mathlib.Algebra.Homology.Homotopy
_private.Mathlib.Algebra.Homology.Homotopy.0.Homotopy.mkInductiveAux₂.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Lean.Meta.Tactic.Subst
/-- Given `x`, try to find an equation of the form `heq : x = rhs` or `heq : lhs = x`,
and runs `substCore` on it. Returns `none` if no such equation is found, or if `substCore` fails.
 -/
Lean.Meta.substVar? : Lean.MVarId → Lean.FVarId → Lean.MetaM (Option Lean.MVarId)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_of_isEmpty : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, m.isEmpty = true → m.contains a = false
-- Mathlib.Analysis.Normed.Module.Basic
/-- The action of the original `NormedField` on `RestrictScalars 𝕜 𝕜' E`.
This is not an instance as it would be contrary to the purpose of `RestrictScalars`.
 -/
Module.RestrictScalars.normedAlgebraOrig : {𝕜 : Type u_6} →
  {𝕜' : Type u_7} →
    {E : Type u_8} →
      [inst : NormedField 𝕜'] →
        [inst_1 : SeminormedRing E] → [I : NormedAlgebra 𝕜' E] → NormedAlgebra 𝕜' (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_orbit_iff : ∀ {γ : Type u_2} {α : Type u_3} [inst : VAdd γ α] {a₁ a₂ : α}, a₂ ∈ AddAction.orbit γ a₁ ↔ ∃ x, x +ᵥ a₁ = a₂
-- Init.Data.Rat.Basic
Rat.instOfScientific : OfScientific ℚ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.inv_nonempty_iff`. -/
Finset.Nonempty.inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α}, s.Nonempty → s⁻¹.Nonempty
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.MorphismProperty.transfiniteCompositions_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u} W ≤ W.rlp.llp
-- Mathlib.Combinatorics.Graph.Basic
Graph.eq_bouquet_iff : ∀ {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β}, G = Graph.bouquet v G.edgeSet ↔ G.vertexSet = {v}
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Checks that for each clause `c ∈ f` such that `(Literal.negate pivot) ∈ c`, `c`'s index is in
`ratHints.map (fun x => x.1)`. This function assumes that ratHints are ordered by the value of their
first argument, which is consistent with LRAT's specification
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratHintsExhaustive : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Array (ℕ × Array ℕ) → Bool
-- Mathlib.Data.Int.LeastGreatest
Int.coe_greatestOfBdd_eq : ∀ {P : ℤ → Prop} [inst : DecidablePred P] {b b' : ℤ} (Hb : ∀ (z : ℤ), P z → z ≤ b) (Hb' : ∀ (z : ℤ), P z → z ≤ b')
  (Hinh : ∃ z, P z), ↑(b.greatestOfBdd Hb Hinh) = ↑(b'.greatestOfBdd Hb' Hinh)
-- Mathlib.Topology.Inseparable
SpecializingMap.stableUnderSpecialization_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  SpecializingMap f → ∀ {s : Set X}, StableUnderSpecialization s → StableUnderSpecialization (f '' s)
-- Mathlib.Geometry.Manifold.Instances.Real
interior_halfSpace : ∀ {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n), interior {y | a ≤ y.ofLp i} = {y | a < y.ofLp i}
-- Mathlib.Analysis.Convex.MetricSpace
/-- `dist(sx + (1-s)y, sx' + (1-s)y') ≤ s dist(x, x') + (1-s) dist(y, y')`.

See `dist_convexCombPair_convexCombPair`
for the version where the points are fixed and the weights change.  -/
Convexity.dist_convexCombPair_convexCombPair_le : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {s t : ℝ}
  (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y x' y' : X),
  dist (Convexity.convexCombPair s t hs ht h x y) (Convexity.convexCombPair s t hs ht h x' y') ≤
    s * dist x x' + t * dist y y'
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.indep_biSup_compl : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iIndep s μ → ∀ (t : Set ι), ProbabilityTheory.Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) μ
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_lift_snd_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c}
  (α : M ⟶ K) (β : M ⟶ L) (i : ι),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift α β).f i)
      (CategoryTheory.Limits.biprod.snd.f i) =
    β.f i
-- Init.Data.Vector.Lemmas
/-- Variant of `all_eq_true` in terms of membership rather than an array index.  -/
Vector.all_eq_true' : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.all p = true ↔ ∀ x ∈ xs, p x = true
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termF₃ : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.Defs
CancelMonoidWithZero.toIsCancelMulZero : ∀ {M₀ : Type u_2} (self : CancelMonoidWithZero M₀), IsCancelMulZero M₀
-- Mathlib.Data.Set.Basic
Set.mem_bijective : ∀ {α : Type u}, Function.Bijective Membership.mem
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Noncomputable model function returning the start point of the longest match ending at the given
position, or `none` if there is no match.
 -/
String.Slice.Pattern.Model.revMatchAt? : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → Option s.Pos
-- Mathlib.Tactic.ENatToNat
Mathlib.Tactic.ENatToNat.coe_one : 1 = ↑1
-- Batteries.Recycling.RBTree.Basic
/-- `O(n log n)`. Build a tree from an unsorted array by inserting them one at a time.  -/
RBTree.RBSet.ofArray : {α : Type u_1} → Array α → (cmp : α → α → Ordering) → RBTree.RBSet α cmp
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.factor_evalₐ_eq_eval : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {n : ℕ} (x : AdicCompletion I R) (h : I ^ n ≤ I ^ n • ⊤),
  (Ideal.Quotient.factor h) ((AdicCompletion.evalₐ I n) x) = (AdicCompletion.eval I R n) x
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.brecOn_2.go : {motive_1 : Lean.IR.IRType → Sort u} →
  {motive_2 : Array Lean.IR.IRType → Sort u} →
    {motive_3 : List Lean.IR.IRType → Sort u} →
      (t : List Lean.IR.IRType) →
        ((t : Lean.IR.IRType) → t.below → motive_1 t) →
          ((t : Array Lean.IR.IRType) → Lean.IR.IRType.below_1 t → motive_2 t) →
            ((t : List Lean.IR.IRType) → Lean.IR.IRType.below_2 t → motive_3 t) → motive_3 t ×' Lean.IR.IRType.below_2 t
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The cokernel of `biprod.inr : Y ⟶ X ⊞ Y` is `X`.  -/
CategoryTheory.Limits.cokernelBiprodInrIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.cokernel CategoryTheory.Limits.biprod.inr ≅ X
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Balanced.zoom : ∀ {α : Type u_1} {cut : α → Ordering} {t : RBTree.RBNode α} {path : RBTree.RBNode.Path α} {t' : RBTree.RBNode α}
  {path' : RBTree.RBNode.Path α} {c₀ : RBTree.RBColor} {n₀ : ℕ} {c : RBTree.RBColor} {n : ℕ},
  t.Balanced c n →
    RBTree.RBNode.Path.Balanced c₀ n₀ path c n →
      RBTree.RBNode.zoom cut t path = (t', path') → ∃ c n, t'.Balanced c n ∧ RBTree.RBNode.Path.Balanced c₀ n₀ path' c n
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A `HomologicalComplex V c` with a "shape" controlled by `c : ComplexShape ι`
has chain groups `X i` (objects in `V`) indexed by `i : ι`,
and a differential `d i j` whenever `c.Rel i j`.

We in fact ask for differentials `d i j` for all `i j : ι`,
but have a field `shape` requiring that these are zero when not allowed by `c`.
This avoids a lot of dependent type theory hell!

The composite of any two differentials `d i j ≫ d j k` must be zero.
 -/
HomologicalComplex : {ι : Type u_1} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [CategoryTheory.Limits.HasZeroMorphisms V] → ComplexShape ι → Type (max (max u u_1) v)
-- Mathlib.Logic.Basic
ne_or_eq : ∀ {α : Sort u_1} (x y : α), x ≠ y ∨ x = y
-- Init.Data.Array.Subarray
/-- The stopping index is no later than the end of the array.

The ending index is exclusive. If it is equal to the size of the array, then the last element of
the array is in the subarray.
 -/
Subarray.stop_le_array_size : ∀ {α : Type u_1} (xs : Subarray α), xs.stop ≤ xs.array.size
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverUnitPullback_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X X_1 : C),
  ((CategoryTheory.toOverUnitPullback X).hom.app X_1).left =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 X)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesColimitπ₃ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)],
  CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₃
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space  -/
SubMulAction.stabilizer_of_subMul.submonoid : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : ↥p),
  MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R ↑m
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The dependent coevaluation natural transformation as the unit of the adjunction.  -/
CategoryTheory.ExponentiableMorphism.coev : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J : C} →
      (f : I ⟶ J) →
        [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
          [inst_2 : CategoryTheory.ExponentiableMorphism f] →
            CategoryTheory.Functor.id (CategoryTheory.Over J) ⟶
              (CategoryTheory.ChosenPullbacksAlong.pullback f).comp (CategoryTheory.ExponentiableMorphism.pushforward f)
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.corootSpace.eq_1 : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} [inst_3 : LieRing.IsNilpotent ↥H] [inst_4 : H.IsCartanSubalgebra] [inst_5 : IsNoetherian R L]
  (α : ↥H → R),
  LieAlgebra.corootSpace α =
    (LieModuleHom.codRestrict H.toLieSubmodule
        ((LieAlgebra.rootSpace H 0).incl.comp (LieAlgebra.rootSpaceProduct R L H α (-α) 0 ⋯)) ⋯).range
-- Lean.Data.Json.FromToJson.Extra
Lean.instToJsonTreeMapStringCompare : {α : Type u_1} → [Lean.ToJson α] → Lean.ToJson (Std.TreeMap String α compare)
-- Init.Data.Float.Model.Unpacked.Round
Float.Model.UnpackedFloat.ExtendedMantissa.mk : ℕ → Bool → Bool → Float.Model.UnpackedFloat.ExtendedMantissa
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.IsProper f],
  AlgebraicGeometry.IsProper (f ∣_ V)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], m₂.contains k = false → (m₁.union m₂).get! k = m₁.get! k
-- Mathlib.Order.Compare
Ordering.Compares.eq_eq : ∀ {α : Type u_1} [inst : Preorder α] {o : Ordering} {a b : α}, o.Compares a b → (o = Ordering.eq ↔ a = b)
-- Mathlib.Algebra.Group.Action.Defs
IsCancelSMul.eq_one_of_smul : ∀ {G : Type u_11} {P : Type u_12} [inst : Monoid G] [inst_1 : MulAction G P] [IsCancelSMul G P] {g : G} {x : P},
  g • x = x → g = 1
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
ciSup_eq_univ_of_not_bddAbove : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {f : ι → α},
  ¬BddAbove (Set.range f) → ⨆ i, f i = sSup Set.univ
-- Mathlib.Data.Semiquot
Semiquot.instLE : {α : Type u_1} → LE (Semiquot α)
-- Init.Data.Sum.Lemmas
Sum.isLeft.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (val : β), (Sum.inr val).isLeft = false
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : CategoryTheory.Sheaf J (Type (max v v'))} (t : F.obj.obj X),
  J.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.obj.map f)) t) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map f.unop)
      (J.uliftYonedaEquiv.symm t)
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicInterior.eq_1 : ∀ (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicInterior 𝕜 s = Subtype.val '' interior (Subtype.val ⁻¹' s)
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.nondegen : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H), self.A.Nondegenerate