mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.right_comm : ∀ {S : Type u_3} [inst : AddSemigroup S] {b c : S}, AddCommute b c → ∀ (a : S), a + b + c = a + c + b
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the denominator of the left fractions  -/
CategoryTheory.MorphismProperty.LeftFraction₂.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction₂ X Y) → Y ⟶ self.Y'
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The inner product of two non-zero vectors equals the negative product of their norms
if and only if the angle between the two vectors is π.  -/
InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 → y ≠ 0 → (inner ℝ x y = -(‖x‖ * ‖y‖) ↔ InnerProductGeometry.angle x y = Real.pi)
-- Mathlib.RingTheory.Localization.Defs
Localization.mk_one_eq_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (x : R),
  Localization.mk x 1 = (algebraMap R (Localization M)) x
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op.eq_1 : ∀ {M : Type u_2} [inst : Mul M] (x : Subsemigroup M), x.op = { carrier := MulOpposite.unop ⁻¹' ↑x, mul_mem' := ⋯ }
-- Mathlib.Data.Fin.Tuple.Basic
Fin.removeNth_zero : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (f : (i : Fin (n + 1)) → α i), Fin.removeNth 0 f = Fin.tail f
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.karoubiUniversal₁_unitIso : ∀ (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],
  (CategoryTheory.Idempotents.karoubiUniversal₁ C D).unitIso =
    (CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso C D).symm
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- A type synonym for a linear order `J`, will be equipped with a simplicial category structure.  -/
CategoryTheory.SimplicialThickening : (J : Type u_1) → [LinearOrder J] → Type u_1
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableSub` if `(c - ·)` and `(· - c)` are measurable
functions. For a typeclass assuming measurability of `uncurry (-)` see `MeasurableSub₂`.  -/
MeasurableSub : (G : Type u_2) → [MeasurableSpace G] → [Sub G] → Prop
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_apply_coe : ∀ {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J (Type u)) (s : I.sections)
  (i : CategoryTheory.Limits.WalkingMulticospan J),
  ↑(I.sectionsEquiv s) i =
    match i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => s.val i
    | CategoryTheory.Limits.WalkingMulticospan.right j =>
      (CategoryTheory.ConcreteCategory.hom (I.fst j)) (s.val (J.fst j))
-- Mathlib.Algebra.Divisibility.Units
not_isUnit_of_not_isUnit_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, ¬IsUnit a → a ∣ b → ¬IsUnit b
-- Std.Async.Basic
/-- Maps the result of an `EAsync` computation with a pure function.
 -/
Std.Async.EAsync.map : {α β ε : Type} → (α → β) → Std.Async.EAsync ε α → Std.Async.EAsync ε β
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Hom.sub.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f g : P.Hom P'),
  f.sub g =
    LinearMap.liftBaseChange S
      (let __spread.0 := ↑R Algebra.Extension.Cotangent.mk ∘ₗ f.subToKer g;
        { toLinearMap := __spread.0, map_one_eq_zero' := ⋯, leibniz' := ⋯ }).liftKaehlerDifferential
-- Mathlib.Data.List.Destutter
List.destutter_singleton : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a : α}, List.destutter R [a] = [a]
-- Init.Meta.Defs
Lean.Syntax.setTailInfo : Lean.Syntax → Lean.SourceInfo → Lean.Syntax
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_counitIso_inv_app_right_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D)))
  (X_1 : C),
  (CategoryTheory.WithInitial.equivComma.counitIso.inv.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithInitial.incl.obj X_1 with
      | CategoryTheory.WithInitial.of x => X.right.obj x
      | CategoryTheory.WithInitial.star => X.left)
-- Lean.Server.References
Lean.Server.References.ParentDecl.mk : String → Lean.Lsp.Range → Lean.Lsp.Range → Lean.Server.References.ParentDecl
-- Mathlib.Topology.Order.WithTop
WithTop.isEmbedding_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  Topology.IsEmbedding WithTop.some
-- Batteries.Data.List.Lemmas
List.idxOfNth_cons_zero_of_beq : ∀ {α : Type u_1} {x : α} {xs : List α} {a : α} [inst : BEq α], (a == x) = true → List.idxOfNth x (a :: xs) 0 = 0
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- The discriminant of a linear polynomial is `1`.  -/
Polynomial.discr_of_degree_eq_one : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R}, f.degree = 1 → f.discr = 1
-- Mathlib.Data.Set.Function
Set.InjOn.prodMap : ∀ {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {f₁ : α₁ → β₁}
  {f₂ : α₂ → β₂}, Set.InjOn f₁ s₁ → Set.InjOn f₂ s₂ → Set.InjOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`.  -/
AddSubgroup.inclusion : {G : Type u_1} → [inst : AddGroup G] → {H K : AddSubgroup G} → H ≤ K → ↥H →+ ↥K
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map_injective : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (h : M →ₗ[R] N),
  Function.Injective ⇑h → Function.Injective ⇑((IsLocalizedModule.map S f g) h)
-- Mathlib.NumberTheory.LucasLehmer
/-- If `3` is not a square then `(1 + α) ^ (q + 1) = -2`.  -/
LucasLehmer.X.one_add_α_pow_q_succ : ∀ {q : ℕ} [inst : Fact (Nat.Prime q)], Odd q → legendreSym q 3 = -1 → (1 + LucasLehmer.X.α) ^ (q + 1) = -2
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanHom_zero_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsMulFreimanHom 0 A B f ↔ Set.MapsTo f A B
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- The real-valued version of a measure. Maps infinite measure sets to zero. Use as `μ.real s`.
The API is developed in `Mathlib/MeasureTheory/Measure/Real.lean`.  -/
MeasureTheory.Measure.real : {α : Type u_6} → {m : MeasurableSpace α} → MeasureTheory.Measure α → Set α → ℝ
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instStarAddMonoid : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddMonoid β] →
          [inst_3 : StarAddMonoid β] →
            [ContinuousStar β] → [inst_5 : ContinuousAdd β] → StarAddMonoid (CompactlySupportedContinuousMap α β)
-- Std.Do.PostCond
/-- A postcondition expressing total correctness.
That is, it expresses that the asserted computation finishes without throwing an exception
*and* the result satisfies the given predicate `p`.
 -/
Std.Do.PostCond.noThrow : {α : Type u_1} → {ps : Std.Do.PostShape} → (α → Std.Do.Assertion ps) → Std.Do.PostCond α ps
-- Mathlib.Algebra.Group.Defs
/-- One is a right neutral element for multiplication  -/
MulOneClass.mul_one : ∀ {M : Type u} [self : MulOneClass M] (a : M), a * 1 = a
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofNat' : ∀ (n : ℕ), (UInt64.ofNat n).toUInt32 = UInt32.ofNat n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {a : α}, ∅.getKey! a = default
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckRightact : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.coe_ofEq_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  {p q : Submodule R M} (h : p = q) (x : ↥p), ↑((LinearEquiv.ofEq p q h) x) = ↑x
-- Mathlib.LinearAlgebra.Pi
LinearMap.vecEmpty₂_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (x : M), LinearMap.vecEmpty₂ x = LinearMap.vecEmpty
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.step.match_1.congr_eq_1 : ∀ {Γ : Type u_1} (motive : Turing.TM0.Stmt Γ → Sort u_2) (a : Turing.TM0.Stmt Γ)
  (h_1 : (d : Turing.Dir) → motive (Turing.TM0.Stmt.move d)) (h_2 : (a : Γ) → motive (Turing.TM0.Stmt.write a))
  (d : Turing.Dir),
  a = Turing.TM0.Stmt.move d →
    (match a with
      | Turing.TM0.Stmt.move d => h_1 d
      | Turing.TM0.Stmt.write a => h_2 a) ≍
      h_1 d
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.decidableMemAdd : {α : Type u_2} →
  [inst : AddMonoid α] →
    {s t : Set α} →
      [Fintype α] →
        [DecidableEq α] →
          [DecidablePred fun x => x ∈ s] → [DecidablePred fun x => x ∈ t] → DecidablePred fun x => x ∈ s + t
-- Mathlib.Analysis.Convex.Hull
mem_convexHull_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E} {x : E}, x ∈ (convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The second leg of a pullback cone is a regular monomorphism if the right component is too.

See also `Pullback.sndOfMono` for the basic monomorphism version, and
`regularOfIsPullbackFstOfRegular` for the flipped version.
 -/
CategoryTheory.regularOfIsPullbackSndOfRegular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P Q R S : C} →
      {f : P ⟶ Q} →
        {g : P ⟶ R} →
          {h : Q ⟶ S} →
            {k : R ⟶ S} →
              CategoryTheory.RegularMono h →
                (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm) →
                    CategoryTheory.RegularMono g
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNegZeroClass.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : NegZeroClass G] [inst_2 : ContinuousNeg G],
  SeparationQuotient.instNegZeroClass =
    { toZero := SeparationQuotient.instZero, toNeg := SeparationQuotient.instNeg, neg_zero := ⋯ }
-- Mathlib.Topology.Sets.Closeds
/-- `TopologicalSpace.Opens.compl` as an `OrderIso` to the order dual of
`TopologicalSpace.Closeds α`.  -/
TopologicalSpace.Opens.complOrderIso : (α : Type u_2) → [inst : TopologicalSpace α] → TopologicalSpace.Opens α ≃o (TopologicalSpace.Closeds α)ᵒᵈ
-- Mathlib.Tactic.Translate.Core
/-- the `(relevant_arg := ...)` option tells which argument to look at to determine whether to
translate this constant. This is inferred automatically,
but it can also be overwritten using this syntax.

If there are multiple possible arguments, we typically tag the first one.
If this argument contains a fixed type, this declaration will not be translated.
See the Heuristics section of the `to_additive` doc-string for more details.

When it cannot be inferred automatically, it is presumed that the first argument is relevant.

Use `(relevant_arg := _)` to indicate that there is no relevant argument.

Implementation note: we only allow exactly 1 relevant argument, even though some declarations
(like `Prod.instGroup`) have multiple relevant arguments.
The reason is that whether we translate a declaration is an all-or-nothing decision, and
we will not be able to translate declarations that (e.g.) talk about multiplication on `ℕ × α`
anyway.
 -/
Mathlib.Tactic.Translate.relevantArgOption : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Fin.Basic
/-- A product space `α × β` is equivalent to the space `Π i : Fin 2, γ i`, where
`γ = Fin.cons α (Fin.cons β finZeroElim)`. See also `piFinTwoEquiv` and
`finTwoArrowEquiv`.  -/
prodEquivPiFinTwo : (α β : Type u) → α × β ≃ ((i : Fin 2) → ![α, β] i)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The variant of `is_left_invariant_addCHaar` for `addHaarContent`  -/
MeasureTheory.Measure.haar.is_left_invariant_addHaarContent : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G),
  (MeasureTheory.Measure.haar.addHaarContent K₀) (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) =
    (MeasureTheory.Measure.haar.addHaarContent K₀) K
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_zsmul : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (b : ℤ) (v : Π₀ (i : ι), β i), ⇑(b • v) = b • ⇑v
-- Mathlib.RingTheory.AdjoinRoot
/-- The adjoined root.  -/
AdjoinRoot.root : {R : Type u_1} → [inst : CommRing R] → (f : Polynomial R) → AdjoinRoot f
-- Mathlib.Topology.NatEmbedding
/-- If `X` is an infinite Hausdorff topological space, then there exists an infinite set `s : Set X`
that has the induced topology is the discrete topology.  -/
exists_infinite_discreteTopology : ∀ (X : Type u_1) [inst : TopologicalSpace X] [T2Space X] [Infinite X], ∃ s, s.Infinite ∧ DiscreteTopology ↑s
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDerivWithin_neg_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {x : E} {i : ℕ} {f : E → F},
  UniqueDiffOn 𝕜 s → x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- **Alias** of `CategoryTheory.Triangulated.TStructure.isLE_of_le`. -/
CategoryTheory.Triangulated.TStructure.isLE_of_LE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (p q : ℤ),
  autoParam (p ≤ q) CategoryTheory.Triangulated.TStructure.isLE_of_le._auto_1 → ∀ [t.IsLE X p], t.IsLE X q
-- Mathlib.Topology.Algebra.UniformRing
/-- A shortcut instance for the common case  -/
UniformSpace.Completion.algebra' : (R : Type u_2) →
  [inst : CommRing R] →
    [inst_1 : UniformSpace R] →
      [inst_2 : IsUniformAddGroup R] → [inst_3 : IsTopologicalRing R] → Algebra R (UniformSpace.Completion R)
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
AddSubgroup.addSubgroupOfContinuousAddEquivOfLe.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {H K : AddSubgroup G} (hHK : H ≤ K),
  AddSubgroup.addSubgroupOfContinuousAddEquivOfLe hHK = (AddSubgroup.addSubgroupOfEquivOfLe hHK).toContinuousAddEquiv ⋯
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.instMonoidalDiscreteFunctorFunctorF : (C : Type u) →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] → (h : CategoryTheory.ShiftMkCore C A) → (CategoryTheory.Discrete.functor h.F).Monoidal
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHaveIdDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instTop.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Subgroup.instTop =
    {
      top :=
        let __src := ⊤;
        { toSubmonoid := __src, inv_mem' := ⋯ } }
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ici_add_Ioi_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b : α),
  Set.Ici a + Set.Ioi b ⊆ Set.Ioi (a + b)
-- Mathlib.NumberTheory.Dioph
Dioph.ext : ∀ {α : Type u} {S S' : Set (α → ℕ)}, Dioph S → (∀ (v : α → ℕ), v ∈ S ↔ v ∈ S') → Dioph S'
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_of_singleton_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {a : α},
  Function.Bijective ⇑(SubAddAction.ofFixingAddSubgroup_of_singleton M a)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_self_mul : ∀ {α : Type u} [inst : Mul α] [inst_1 : LE α] [CanonicallyOrderedMul α] {a b : α}, a ≤ a * b
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_comp_neg_X : ∀ (n : ℕ),
  (Polynomial.bernoulli n).comp (-Polynomial.X) = (-1) ^ n • (Polynomial.bernoulli n + n • Polynomial.X ^ (n - 1))
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.root?.eq_2 : ∀ {α : Type u_1} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.node c l v r).root? = some v
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.contMDiff_denom_zpow : ∀ {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ) (k : ℤ),
  ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun x => UpperHalfPlane.denom g ↑x ^ k
-- Lean.Parser.Extra
Lean.Parser.nameLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Center
Set.one_mem_center : ∀ {M : Type u_1} [inst : MulOneClass M], 1 ∈ Set.center M
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `M` and `M'` lie in the same universe, the `S`-rank of `M ⊗[R] M'` is
`(Module.rank S M) * (Module.rank R M')`.  -/
rank_tensorProduct' : ∀ {R : Type u} {S : Type u'} {M M₁ : Type v} [inst : Semiring R] [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M] [StrongRankCondition R] [StrongRankCondition S]
  [inst_7 : Module S M] [inst_8 : Module S M₁] [Module.Free S M₁] [inst_10 : Algebra S R]
  [inst_11 : IsScalarTower S R M] [Module.Free R M],
  Module.rank R (TensorProduct S M M₁) = Module.rank R M * Module.rank S M₁
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.add_snd : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x y : WithCStarModule A (E × F)) [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F], (x + y).2 = x.2 + y.2
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.ker_baseChange_comp_cancelBaseChange_symm : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module A N]
  (f : TensorProduct R A M →ₗ[A] N),
  (LinearMap.baseChange A f ∘ₗ ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A A A M).symm).ker = f.ker
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that the intersection according to `Roc.HasRcoIntersection`
of two ranges contains exactly those elements that are contained in both ranges.
 -/
Std.Roc.LawfulRcoIntersection : (α : Type w) → [LT α] → [LE α] → [Std.Roc.HasRcoIntersection α] → Prop
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRicSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRicSlice._auto_1) →
      Std.Ric.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RicSlice α β)
-- Mathlib.Data.Finmap
AList.toFinmap_eq : ∀ {α : Type u} {β : α → Type v} {s₁ s₂ : AList β}, s₁.toFinmap = s₂.toFinmap ↔ s₁.entries.Perm s₂.entries
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundOptionTExceptPUnitPureOfLawfulMonad.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_iff_exists_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₂ : P}, p₂ ∈ s → (s.WOppSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getKey? a = if compare k a = Ordering.eq then none else t.getKey? a
-- Mathlib.Tactic.Translate.Reorder
/-- Permute an array of arguments using the given reorder.  -/
Mathlib.Tactic.Translate.Permutation.permute! : {α : Type u_1} → [Inhabited α] → Mathlib.Tactic.Translate.Permutation → Array α → Array α
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) {a b : B'}
  {f g : a ⟶ b} (f_1 : f ⟶ g),
  ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).map₂ f_1).iso.inv = CategoryTheory.inv (F.map₂ f_1)
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_extractLsb'_of_le : ∀ {w len₁ len₂ start : ℕ} {c : BitVec w},
  len₁ ≤ len₂ → BitVec.setWidth len₁ (BitVec.extractLsb' start len₂ c) = BitVec.extractLsb' start len₁ c
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.volume_pi_eq_dirac : ∀ {ι : Type u_4} [inst : Fintype ι] [inst_1 : IsEmpty ι] {α : ι → Type u_5}
  [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (α i)] (x : optParam ((a : ι) → α a) fun a => isEmptyElim a),
  MeasureTheory.volume = MeasureTheory.Measure.dirac x
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.orderHom_top : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N] (f : M →*o N),
  (MulArchimedeanClass.orderHom f) ⊤ = ⊤
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ),
  Polynomial.derivative (Polynomial.C a * Polynomial.X ^ n) = Polynomial.C (a * ↑n) * Polynomial.X ^ (n - 1)
-- Lean.Declaration
Lean.Declaration.mutualDefnDecl : List Lean.DefinitionVal → Lean.Declaration
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₂_ext_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G}
  {f₁ f₂ : ↥(groupCohomology.coboundaries₂ A)}, f₁ = f₂ ↔ ∀ (g h : G), f₁ (g, h) = f₂ (g, h)
-- Init.Data.List.Basic
List.span.loop : {α : Type u} → (α → Bool) → List α → List α → List α × List α
-- Mathlib.Analysis.Convex.Independent
Convex.convexIndependent_extremePoints : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ConvexIndependent 𝕜 Subtype.val