mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Tactics
/-- * `clear_value x...` clears the values of the given local definitions.
  A local definition `x : α := v` becomes a hypothesis `x : α`.

* `clear_value (h : x = _)` adds a hypothesis `h : x = v` before clearing the value of `x`.
  This is short for `have h : x = v := rfl; clear_value x`.
  Any value definitionally equal to `v` can be used in place of `_`.

* `clear_value *` clears values of all hypotheses that can be cleared.
  Fails if none can be cleared.

These syntaxes can be combined. For example, `clear_value x y *` ensures that `x` and `y` are cleared
while trying to clear all other local definitions,
and `clear_value (hx : x = _) y * with hx` does the same while first adding the `hx : x = v` hypothesis.
 -/
Lean.Parser.Tactic.clearValue : Lean.ParserDescr
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isNNRat_nnratCast : ∀ {R : Type u_1} [inst : DivisionSemiring R] [CharZero R] {q : ℚ≥0} {n d : ℕ},
  Mathlib.Meta.NormNum.IsNNRat q n d → Mathlib.Meta.NormNum.IsNNRat (↑q) n d
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_sub : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Sub α] (s : ι → Set α) (t : Set α), (⋃ i, s i) - t = ⋃ i, s i - t
-- Mathlib.FieldTheory.IsPerfectClosure
pNilradical_eq_bot_of_frobenius_inj : ∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p],
  Function.Injective ⇑(frobenius R p) → pNilradical R p = ⊥
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- `gal p` embeds as a subgroup of permutations of the roots of `p` in `E`.  -/
Polynomial.Gal.galActionHom_injective : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits], Function.Injective ⇑(Polynomial.Gal.galActionHom p E)
-- Mathlib.Order.Heyting.Basic
disjoint_compl_compl_left_iff : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, Disjoint aᶜᶜ b ↔ Disjoint a b
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.inf_subgroupOf_inf_normal_of_right : ∀ {G : Type u_1} [inst : Group G] (A B' B : Subgroup G) [hN : (B'.subgroupOf B).Normal],
  ((A ⊓ B').subgroupOf (A ⊓ B)).Normal
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_eq_top_iff : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  [inst_3 : RingHomClass F R S] {I : Ideal S}, Ideal.comap f I = ⊤ ↔ I = ⊤
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dShortComplex_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_7),
  (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).X₂ = X.E f₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_functor_obj_hom : ∀ {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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R),
  ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).hom =
    CategoryTheory.CategoryStruct.comp (i.inv.app X.left) X.hom
-- Mathlib.Analysis.Calculus.TangentCone.Basic
tangentConeAt_mono_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s t : Set E}
  {x : E} [ContinuousAdd E], nhdsWithin x s ≤ nhdsWithin x t → tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Types.instSmallJointlySurjectivePrecoverage : CategoryTheory.Types.jointlySurjectivePrecoverage.Small
-- Lean.Util.LeanOptions
/-- An option that is used by Lean as if it was passed using `-D`.  -/
Lean.LeanOption : Type
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inr_snd_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inr (CategoryTheory.CategoryStruct.comp self.snd h) = h
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.subsingleton_of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (hX : CategoryTheory.Limits.IsInitial X),
  Subsingleton (CategoryTheory.Subobject X)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- A set in `E` which is open in the weak topology is open.  -/
WeakSpace.isOpen_of_isOpen : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (V : Set E), IsOpen (⇑(toWeakSpaceCLM 𝕜 E) '' V) → IsOpen V
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integrableOn_iUnion_of_summable_integral_norm : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} {ι : Type u_5} [Countable ι] {μ : MeasureTheory.Measure X}
  [inst : NormedAddCommGroup E] {f : X → E} {s : ι → Set X},
  (∀ (i : ι), MeasureTheory.IntegrableOn f (s i) μ) →
    (Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ) → MeasureTheory.IntegrableOn f (Set.iUnion s) μ
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.ι_preservesColimitIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G]
  [inst_4 : CategoryTheory.Limits.HasColimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.ι F j))
      (CategoryTheory.preservesColimitIso G F).hom =
    CategoryTheory.Limits.colimit.ι (F.comp G) j
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α} {hc : t.maxKeyD fallback ∈ t}, t.getKey (t.maxKeyD fallback) hc = t.maxKeyD fallback
-- Mathlib.Topology.Algebra.Module.Equiv
/-- `ContinuousSemilinearEquivClass F σ M M₂` asserts `F` is a type of bundled continuous
`σ`-semilinear equivs `M → M₂`.  See also `ContinuousLinearEquivClass F R M M₂` for the case
where `σ` is the identity map on `R`.  A map `f` between an `R`-module and an `S`-module over a ring
homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y`
and `f (c • x) = (σ c) • f x`.  -/
ContinuousSemilinearEquivClass.inv_continuous : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ}
  {M : outParam (Type u_4)} {inst_4 : TopologicalSpace M} {inst_5 : AddCommMonoid M} {M₂ : outParam (Type u_5)}
  {inst_6 : TopologicalSpace M₂} {inst_7 : AddCommMonoid M₂} {inst_8 : Module R M} {inst_9 : Module S M₂}
  {inst_10 : EquivLike F M M₂} [self : ContinuousSemilinearEquivClass F σ M M₂] (f : F), Continuous (EquivLike.inv f)
-- Mathlib.Topology.Constructions
IsOpen.isOpenMap_inclusion : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → ∀ (h : s ⊆ t), IsOpenMap (Set.inclusion h)
-- Std.Do.WP.Sound
/-- A `wp`-provable postcondition with split `some`/`none` cases refines the post-run computation
`prog.run : m (Option α)` via `Internal.Ensures`.
 -/
Std.Do.OptionT.ensures_of_wp_run : ∀ {m : Type u → Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m Std.Do.PostShape.pure]
  [Std.Do.WPSound m Std.Do.PostShape.pure] {α : Type u} {prog : OptionT m α} (P : Option α → Prop),
  (⊢ₛ (Std.Do.wp prog).apply (fun a => ⌜P (some a)⌝, fun x => ⌜P none⌝, PUnit.unit)) →
    Std.Do.Internal.Ensures P prog.run
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Lnorm : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X] {P : M},
  IsLprojection X P → ∀ (x : X), ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖
-- Mathlib.Topology.Basic
isOpen_biInter_finset : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Finset α} {f : α → Set X},
  (∀ i ∈ s, IsOpen (f i)) → IsOpen (⋂ i ∈ s, f i)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).hom g = f
-- Lean.DocString.Syntax
/-- A URL target, written explicitly. Use square brackets for a named target.  -/
Lean.Doc.Syntax.url : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Scheme
/-- The global sections of `Spec R` is isomorphic to `R`.  -/
AlgebraicGeometry.Scheme.ΓSpecIso : (R : CommRingCat) → (AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤) ≅ R
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.fderiv_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpTo n f p → ∀ {m : ℕ}, ↑m < n → ∀ (x : E), fderiv 𝕜 (fun x => p x m) x = (p x m.succ).curryLeft
-- Init.Grind.Lemmas
Lean.Grind.of_lookahead : ∀ (p : Prop), (¬p → False) → p = True
-- Mathlib.Algebra.GroupWithZero.Associated
associated_eq_eq : ∀ {M : Type u_1} [inst : Monoid M] [Subsingleton Mˣ], Associated = Eq
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `Y`-coordinate of a representative of `-(P + Q)` for two distinct Jacobian point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`.  -/
WeierstrassCurve.Jacobian.negAddY : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → (Fin 3 → R) → R
-- Mathlib.Data.Semiquot
Semiquot.liftOn_ofMem : ∀ {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : α → β) (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b),
  ∀ a ∈ q, q.liftOn f h = f a
-- Mathlib.Order.RelSeries
RelSeries.smash_castAdd : ∀ {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin p.length),
  (p.smash q h).toFun (Fin.castAdd q.length i).castSucc = p.toFun i.castSucc
-- Mathlib.Algebra.Lie.Ideal
/-- Given two nested Lie ideals `I₁ ⊆ I₂`, the inclusion `I₁ ↪ I₂` is a morphism of Lie algebras.  -/
LieIdeal.inclusion : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → {I₁ I₂ : LieIdeal R L} → I₁ ≤ I₂ → ↥I₁ →ₗ⁅R⁆ ↥I₂
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.small_skeleton_of_essentiallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [h : CategoryTheory.EssentiallySmall.{w, v, u} C],
  Small.{w, u} (CategoryTheory.Skeleton C)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.contains t.minKey! = true
-- Lean.Parser.Term
Lean.Parser.Term.explicit.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.proj.inj : ∀ {typeName : Lean.Name} {idx nargs : ℕ} {typeName_1 : Lean.Name} {idx_1 nargs_1 : ℕ},
  Lean.Meta.RefinedDiscrTree.Key.proj typeName idx nargs =
      Lean.Meta.RefinedDiscrTree.Key.proj typeName_1 idx_1 nargs_1 →
    typeName = typeName_1 ∧ idx = idx_1 ∧ nargs = nargs_1
-- Lean.MetavarContext
Lean.DelayedMetavarAssignment.mk.injEq : ∀ (fvars : Array Lean.Expr) (mvarIdPending : Lean.MVarId) (fvars_1 : Array Lean.Expr) (mvarIdPending_1 : Lean.MVarId),
  ({ fvars := fvars, mvarIdPending := mvarIdPending } = { fvars := fvars_1, mvarIdPending := mvarIdPending_1 }) =
    (fvars = fvars_1 ∧ mvarIdPending = mvarIdPending_1)
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.markAsConvGoal : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.neg_hom_apply : ∀ {X Y : AddGrpCat} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Lean.Meta.Basic
Lean.Meta.instDecidableEqProjReductionKind : DecidableEq Lean.Meta.ProjReductionKind
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} {hP : W.NonsingularLift ⟦P⟧}
  (hPz : P 2 ≠ 0),
  { point := ⟦P⟧, nonsingular := hP }.toAffineLift =
    WeierstrassCurve.Affine.Point.some (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) ⋯
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3)
  (h_1 : Unit → motive Lean.PersistentHashMap.Entry.null)
  (h_2 : (k : α) → (v : β) → motive (Lean.PersistentHashMap.Entry.entry k v))
  (h_3 : (node : Lean.PersistentHashMap.Node α β) → motive (Lean.PersistentHashMap.Entry.ref node)),
  (match Lean.PersistentHashMap.Entry.null with
    | Lean.PersistentHashMap.Entry.null => h_1 ()
    | Lean.PersistentHashMap.Entry.entry k v => h_2 k v
    | Lean.PersistentHashMap.Entry.ref node => h_3 node) =
    h_1 ()
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the components of the
natural transformation `F ⟶ H` at `G` are precisely the components of the natural transformation
`G ⋙ F ⟶ G ⋙ H` obtained from the units and counits of the adjunctions.  -/
CategoryTheory.Adjunction.Triple.leftToRight_app_obj_assoc : ∀ {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} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  {X Z : D} (h : H.obj (G.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.leftToRight.app (G.obj X)) h =
    CategoryTheory.CategoryStruct.comp (t.adj₁.counit.app X) (CategoryTheory.CategoryStruct.comp (t.adj₂.unit.app X) h)
-- Lean.Meta.Match.CaseValues
Lean.Meta.instInhabitedCaseValuesSubgoal.default : Lean.Meta.CaseValuesSubgoal
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.instSetLike : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → SetLike (Projectivization.Subspace K V) (Projectivization K V)
-- Mathlib.Data.Sign.Defs
SignType.ofNat_ctorIdx : ∀ (x : SignType), SignType.ofNat x.ctorIdx = x
-- Mathlib.Order.Category.BddOrd
BddOrd.dual_map : ∀ {X Y : BddOrd} (f : X ⟶ Y), BddOrd.dual.map f = BddOrd.ofHom (BoundedOrderHom.dual (BddOrd.Hom.hom f))
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.forward.match_1.eq_2 : ∀ (motive : String.Legacy.Iterator → ℕ → Sort u_1) (it : String.Legacy.Iterator) (n : ℕ)
  (h_1 : (it : String.Legacy.Iterator) → motive it 0)
  (h_2 : (it : String.Legacy.Iterator) → (n : ℕ) → motive it n.succ),
  (match it, n.succ with
    | it, 0 => h_1 it
    | it, n.succ => h_2 it n) =
    h_2 it n
-- Batteries.Recycling.RBTree.Alter
/-- Descend into the right subtree of a black node.  -/
RBTree.RBNode.Path.Balanced.blackR : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1} {x : RBTree.RBNode α} {c₁ : RBTree.RBColor} {n : ℕ} {v : α}
  {parent : RBTree.RBNode.Path α} {c₂ : RBTree.RBColor},
  x.Balanced c₁ n →
    RBTree.RBNode.Path.Balanced c₀ n₀ parent RBTree.RBColor.black (n + 1) →
      RBTree.RBNode.Path.Balanced c₀ n₀ (RBTree.RBNode.Path.right RBTree.RBColor.black x v parent) c₂ n
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.edges_bypass_subset_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.edges ⊆ p.edges
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Meta.Grind.Arith.CommRing.EqCnstr.denoteExpr : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Meta.Grind.Arith.CommRing.EqCnstr → M Lean.Expr
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.instSmallObjOppositeFunctorTypeCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : Cᵒᵖ),
  CategoryTheory.FunctorToTypes.Small.{w, v, v, u} (CategoryTheory.coyoneda.obj X)
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_8 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.leftDistrib =
    ∀ (x y z : K), x * (y + z) = x * y + x * z
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.wasChanged.sizeOf_spec : sizeOf Lean.Widget.DiffTag.wasChanged = 1
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.forEachExprWithExposedLevelMVars.visitLevel : (Lean.Expr → Lean.Elab.TermElabM Unit) → Lean.Level → Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSet.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.integerSet K =
    NumberField.mixedEmbedding.fundamentalCone K ∩ ↑(NumberField.mixedEmbedding.integerLattice K)
-- Mathlib.Topology.Closure
Filter.lift'_interior_le : ∀ {X : Type u} [inst : TopologicalSpace X] (l : Filter X), l.lift' interior ≤ l
-- Init.Grind.Ordered.Int
Lean.Grind.instIsLinearOrderInt : Std.IsLinearOrder ℤ
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_subsingleton_apply : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] [Subsingleton n]
  (A : Matrix n n α) (b : n → α) (i : n), A.cramer b i = b i
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C}
  (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)]
  (i : E.I₀),
  (E.pullbackCoverOfRight f g).f i =
    CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp (E.f i) g) f g
      (CategoryTheory.CategoryStruct.id X) (E.f i) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_of_mem : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {x : M} {i : ι} (hx : x ∈ ℳ i),
  (DirectSum.decompose ℳ) x = (DirectSum.of (fun i => ↥(ℳ i)) i) ⟨x, hx⟩
-- Mathlib.GroupTheory.OrderOfElement
/-- See also `injective_nsmul_iff_not_isOfFinAddOrder`.  -/
not_isOfFinAddOrder_of_injective_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, (Function.Injective fun n => n • x) → ¬IsOfFinAddOrder x
-- Mathlib.Tactic.Sat.FromLRAT
/-- Returns `a` and `pr : v n ↔ a` given a variable index `n`.
These are both lookups into the context
`(a0 .. a(n-1) : Prop) (v) (h1 : v 0 ↔ a0) ... (hn : v (n-1) ↔ a(n-1))`.  -/
Mathlib.Tactic.Sat.buildReify.reifyVar : ℕ → Lean.Expr → Lean.Expr × Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsAddMonHom.instNormalZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G : C} [inst_2 : CategoryTheory.AddGrpObj G], CategoryTheory.IsAddMonHom.Normal CategoryTheory.AddMonObj.zero
-- Init.Data.Nat.Lemmas
Nat.mul_div_eq_iff_dvd : ∀ {n d : ℕ}, d * (n / d) = n ↔ d ∣ n
-- Mathlib.FieldTheory.Normal.Basic
/-- [Stacks Tag 09HU](https://stacks.math.columbia.edu/tag/09HU) (Normal part) -/
Normal.of_isSplittingField : ∀ {F : Type u_1} [inst : Field F] {E : Type u_3} [inst_1 : Field E] [inst_2 : Algebra F E] (p : Polynomial F)
  [hFEp : Polynomial.IsSplittingField F E p], Normal F E
-- Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits
CategoryTheory.instHasLimitsOfShapeGrp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {J : Type w} [inst_2 : CategoryTheory.Category.{u_2, w} J] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Grp C)
-- Init.Data.SInt.Lemmas
Int16.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < 2 ^ 15 → b < 2 ^ 15 → (Int16.ofNat a < Int16.ofNat b ↔ a < b)
-- Init.Data.BitVec.Lemmas
BitVec.add_eq_xor : ∀ {a b : BitVec 1}, a + b = a ^^^ b
-- Std.Net.Addr
Std.Net.IPv4Addr.mk.injEq : ∀ (octets octets_1 : Vector UInt8 4), ({ octets := octets } = { octets := octets_1 }) = (octets = octets_1)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_of_not_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬a ≤ b → Set.uIcc a b = Set.Icc b a
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.ev_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type w'}
  (U : I → C) (γ : CategoryTheory.PresheafOfGroups.OneCocycle G U) (i j : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j),
  γ.ev i j a b = (γ.ev j i b a)⁻¹
-- Lean.Meta.Basic
Lean.Meta.SynthInstanceCache : Type
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
WithLp.borelSpace : ∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X] (Y : Type u_2) [inst_1 : MeasurableSpace Y]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [BorelSpace X] [BorelSpace Y]
  [SecondCountableTopologyEither X Y], BorelSpace (WithLp p (X × Y))
-- Mathlib.Order.RelSeries
/-- To show a proposition `p` for `xs : RelSeries r` it suffices to show it for all singletons
and to show that when `p` holds for `xs` it also holds for `xs` appended with one element.
 -/
RelSeries.inductionOn' : {α : Type u_1} →
  {r : SetRel α α} →
    (motive : RelSeries r → Sort u_3) →
      ((x : α) → motive (RelSeries.singleton r x)) →
        ((p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)) →
          (p : RelSeries r) → motive p
-- Mathlib.Order.Lattice.Nat
Nat.iSup_le_succ' : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
  ⨆ k, ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k ≤ n), u (k + 1)