mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.mul b with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_4 a b
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_nonneg : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {l : List M}, (∀ x ∈ l, 0 ≤ x) → 0 ≤ l.sum
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_zero : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β}, Finsupp.mapDomain f 0 = 0
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Multiset.Nat.antidiagonalTuple_zero_right : ∀ (k : ℕ), Multiset.Nat.antidiagonalTuple k 0 = {0}
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- Any matrix polynomial `p` is equivalent under evaluation to `p %ₘ M.charpoly`; that is, `p`
is equivalent to a polynomial with degree less than the dimension of the matrix.  -/
Matrix.aeval_eq_aeval_mod_charpoly : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (p : Polynomial R), (Polynomial.aeval M) p = (Polynomial.aeval M) (p %ₘ M.charpoly)
-- Lean.Meta.Instances
Lean.Meta.addDefaultInstance : Lean.Name → optParam ℕ 0 → Lean.MetaM Unit
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Iso.mk_hom : ∀ {α β : PartOrdEmb} (e : ↑α ≃o ↑β), (PartOrdEmb.Iso.mk e).hom = PartOrdEmb.ofHom (RelIso.toRelEmbedding e)
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- Pseudoequality is transitive: Just take the pullback. The pullback morphisms will
be epimorphisms since in an abelian category, pullbacks of epimorphisms are epimorphisms.  -/
CategoryTheory.Abelian.pseudoEqual_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C},
  IsTrans (CategoryTheory.Over P) (CategoryTheory.Abelian.PseudoEqual P)
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.inv' : {R : Type u_1} →
  [inst : MonoidWithZero R] →
    [Nontrivial R] →
      [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)] →
        [NoZeroDivisors R] → Inv (OreLocalization (nonZeroDivisors R) R)
-- Mathlib.RingTheory.LaurentSeries
/-- In order to compare `K⟦X⟧` with the valuation subring in the `X`-adic completion of
`K⟮X⟯` we consider its alias as a subring of `K⸨X⸩`.  -/
LaurentSeries.powerSeries_as_subring : (K : Type u_2) → [inst : Field K] → Subring (LaurentSeries K)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- The image of `SL(2, ℤ)` in `GL(2, ℝ)` is arithmetic.  -/
Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL : (Matrix.SpecialLinearGroup.mapGL ℝ).range.IsArithmetic
-- Mathlib.CategoryTheory.Join.Opposites
/-- Characterize (up to a rightOp) the action of the left inclusion on `Join.opEquivFunctor`.  -/
CategoryTheory.Join.InclLeftCompRightOpOpEquivFunctor : (C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Join.inclLeft C D).comp (CategoryTheory.Join.opEquiv C D).functor.rightOp ≅
          (CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).rightOp
-- Mathlib.Tactic.FunProp.Decl
/-- Is `e` a `fun_prop` goal? For example `∀ y z, Continuous fun x ↦ f x y z`  -/
Mathlib.Meta.FunProp.isFunPropGoal : Lean.Expr → Lean.MetaM Bool
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.piEquivOfFintype_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι]
  [inst_4 : Fintype ι] (x : AdicCompletion I ((j : ι) → M j)),
  (AdicCompletion.piEquivOfFintype I M) x = (AdicCompletion.pi I M) x
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `J` is `u`-small, `CommMonCat.{u}` has limits of shape `J`.  -/
CommMonCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J CommMonCat
-- Mathlib.Data.List.Chain
List.isChain_flatten : ∀ {α : Type u_1} {R : α → α → Prop} {L : List (List α)},
  [] ∉ L →
    (List.IsChain R L.flatten ↔
      (∀ l ∈ L, List.IsChain R l) ∧ List.IsChain (fun l₁ l₂ => ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y) L)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_eval_neg_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.eval (-2) (Polynomial.Chebyshev.S R n) = ↑↑n.negOnePow * (↑n + 1)
-- Init.Data.BitVec.Bitblast
BitVec.uppcRec.eq_1 : ∀ {w : ℕ} (x : BitVec w) (hs_2 : 0 < w), x.uppcRec 0 hs_2 = x.msb
-- Aesop.Tree.Tracing
Aesop.Rapp.withHeadlineTraceNode : {α : Type} →
  Aesop.Rapp →
    Aesop.TraceOption →
      Lean.MetaM α → optParam Bool true → optParam (Lean.MessageData → Lean.MetaM Lean.MessageData) pure → Lean.MetaM α
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 y z x)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 z x y)
          (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
            (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))))) =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
      (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z))
-- Mathlib.RingTheory.Trace.Quotient
IsLocalization.AtPrime.equivQuotMaximalIdeal.eq_1 : ∀ {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8) [inst_2 : CommRing Rₚ]
  [inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ],
  IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ =
    (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The 0 of the quotient of an `AddMonoid` by an additive congruence
relation is the equivalence class of the `AddMonoid`'s 0.  -/
AddCon.coe_zero : ∀ {M : Type u_1} [inst : Add M] [inst_1 : Zero M] {c : AddCon M}, ↑0 = 0
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- **Equational criterion for vanishing**
[A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term],
forward direction.

Assume that the $m_i$ generate $M$. If the expression $\sum_i m_i \otimes n_i$
vanishes, then it vanishes trivially.  -/
TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι : Type u_4} [inst_5 : Fintype ι] {m : ι → M} {n : ι → N},
  Submodule.span R (Set.range m) = ⊤ → ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ_0_of_three_eq_zero : ∀ {F : Type u_2} [inst : Field F] [inst_1 : DecidableEq F], 3 = 0 → WeierstrassCurve.ofJ 0 = WeierstrassCurve.ofJ1728 F
-- Init.Data.Array.Lemmas
Array.any_filter : ∀ {α : Type u_1} {xs : Array α} {p q : α → Bool}, (Array.filter p xs).any q = xs.any fun a => p a && q a
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- A dense open set `U : Opens X` induces a partial isomorphism between `U` and `X`.  -/
AlgebraicGeometry.Scheme.Opens.partialIsoOfDense : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → Dense ↑U → (↑U).PartialIso X
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedVAdd.mk : ∀ {G : Type u_3} {P : Type u_4} [inst : LE G] [inst_1 : LE P] [inst_2 : VAdd G P],
  (∀ (a b : P), a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b) →
    (∀ (c d : G), c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a) → IsOrderedVAdd G P
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
pentagonal_lt_pentagonal_neg : ∀ {k : ℤ}, 0 < k → pentagonal k < pentagonal (-k)
-- Lean.Util.ParamMinimizer
/-- Found a non minimal solution.  -/
Lean.Util.ParamMinimizer.Status.approx : Lean.Util.ParamMinimizer.Status
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.instUniversallyClosedMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.UniversallyClosed f],
  AlgebraicGeometry.UniversallyClosed (f ∣_ V)
-- Lean.Util.LeanOptions
Lean.instReprLeanOptions.repr : Lean.LeanOptions → ℕ → Std.Format
-- Mathlib.Order.ULift
ULift.up_beq : ∀ {α : Type u} [inst : BEq α] (a b : α), ({ down := a } == { down := b }) = (a == b)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.exact_map_δ : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Function.Exact ⇑(Algebra.Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom)
    ⇑(Algebra.Generators.H1Cotangent.δ Q P)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.mem_of_mem_roo : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {a b : α}, r.lower ≤ b → (a ∈ b<...r.upper) → a ∈ r
-- Init.Data.SInt.Lemmas
Int32.toBitVec_mod : ∀ {a b : Int32}, (a % b).toBitVec = a.toBitVec.srem b.toBitVec
-- Std.Internal.UV.System
/-- Gets all environment variables.
 -/
Std.Internal.UV.System.osEnviron : IO (Array (String × String))
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F` preserves colimits of `K` (written as `PreservesColimit K F`)
if `F` maps any colimit cocone over `K` to a colimit cocone.
 -/
CategoryTheory.Limits.PreservesColimit : {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] → CategoryTheory.Functor J C → CategoryTheory.Functor C D → Prop
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.iterFromIdxM.eq_1 : ∀ {α : Type w} (array : Array α) (m : Type w → Type w') (pos : ℕ) [inst : Pure m],
  array.iterFromIdxM m pos = { internalState := { array := array, pos := pos } }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_eq_not_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey?.isSome = !t.isEmpty
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- An indexed family is said to be affinely independent if no nontrivial weighted subtractions
(where the sum of weights is 0) are 0.  -/
AffineIndependent : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → {ι : Type u_4} → (ι → P) → Prop
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.min? = some km → t.get? km = some km
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.top_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X), ⊤ f
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.target.sizeOf_spec : ∀ (a : Lean.SubExpr.Pos), sizeOf (Lean.SubExpr.GoalLocation.target a) = 1 + sizeOf a
-- Mathlib.Probability.Martingale.BorelCantelli
/-- One-sided martingale bound: If `f` is a submartingale which has uniformly bounded differences,
then for almost every `ω`, `f n ω` is bounded above (in `n`) if and only if it converges.  -/
MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
      ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
-- Mathlib.Data.Sum.Basic
Sum.getLeft.hcongr_4 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (β β' : Type u_2),
      β = β' →
        ∀ (ab : α ⊕ β) (ab' : α' ⊕ β'),
          ab ≍ ab' → ∀ (a : ab.isLeft = true) (a' : ab'.isLeft = true), a ≍ a' → ab.getLeft a ≍ ab'.getLeft a'
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.power_le_power_right : ∀ {a b c : Cardinal.{u_1}}, a ≤ b → a ^ c ≤ b ^ c
-- Mathlib.Algebra.Ring.Basic
one_div_neg_eq_neg_one_div : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] (a : R), 1 / -a = -(1 / a)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_right_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.meet (Lean.Order.meet P Q) R = Lean.Order.meet (Lean.Order.meet P R) Q
-- Batteries.Data.Array.Lemmas
/-- **Alias** of `Array.getElem_insertIdx_of_lt`. -/
Array.getElem_insertIdx_lt : ∀ {α : Type u} {xs : Array α} {x : α} {i k : ℕ} (w : i ≤ xs.size) (h : k < i), (xs.insertIdx i x w)[k] = xs[k]
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If `R` satisfies the strong rank condition,
then for any linearly independent family `v : ι → M`
contained in the span of some finite `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
 -/
linearIndependent_le_span' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} (v : ι → M),
  LinearIndependent R v →
    ∀ (w : Set M) [inst_4 : Fintype ↑w], Set.range v ⊆ ↑(Submodule.span R w) → Cardinal.mk ι ≤ ↑(Fintype.card ↑w)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply_eq_of_inter_support_eq : ∀ {α : Type u_1} (p : PMF α) {s t : Set α}, s ∩ p.support = t ∩ p.support → p.toOuterMeasure s = p.toOuterMeasure t
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioc₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => x * c) ⁻¹' Set.Ioc a b = Set.Ioc (a / c) (b / c)
-- Mathlib.MeasureTheory.Group.Defs
/-- A measure `μ` on a measurable additive group is left invariant
if the measure of left translations of a set are equal to the measure of the set itself.  -/
MeasureTheory.Measure.IsAddLeftInvariant : {G : Type u_1} → [inst : MeasurableSpace G] → [Add G] → MeasureTheory.Measure G → Prop
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_inter' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, t ∈ nhdsWithin x s → (ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSMul.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α], Colex.instSMul = inst
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balance2.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d)))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive a x (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d))
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (match a, x, RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d) with
    | a, x, RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d) => h_1 a x b y c z d
    | a, x, RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z d => h_2 a x b y c z d
    | a, x, b => h_3 a x b) =
    h_1 a x b y c z d
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.instAdditiveObjFunctorAdditiveFunctor_1 : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : C ⥤+ D), F.obj.Additive
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.SigmaFinite.withDensity_ofReal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (f : α → ℝ),
  MeasureTheory.SigmaFinite (μ.withDensity fun x => ENNReal.ofReal (f x))
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.ext : ∀ {μ : YoungDiagram} {T T' : SemistandardYoungTableau μ}, (∀ (i j : ℕ), T i j = T' i j) → T = T'
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- A space with `MeasurableSpace` and `TopologicalSpace` structures such that
all open sets are measurable.  -/
OpensMeasurableSpace : (α : Type u_6) → [TopologicalSpace α] → [h : MeasurableSpace α] → Prop
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.l_surjective : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisInsertion l u), Function.Surjective l
-- Std.Internal.Do.Order.Basic
Lean.Order.join_le : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (x y z : α),
  Lean.Order.PartialOrder.rel x z →
    Lean.Order.PartialOrder.rel y z → Lean.Order.PartialOrder.rel (Lean.Order.join x y) z
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valuation.inversion_estimate' : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) {x y r s : K},
  y ≠ 0 → r ≠ 0 → s ≠ 0 → v (x - y) < min (v s / v r * (v y * v y)) (v y) → v (x⁻¹ - y⁻¹) * v r < v s
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.toMonad_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R),
  h.toMonad.μ = CategoryTheory.Functor.whiskerRight (L.whiskerLeft h.counit) R
-- Init.Data.SInt.Bitwise
Int32.not_eq_comm : ∀ {a b : Int32}, ~~~a = b ↔ a = ~~~b
-- Init.Data.Rat.Basic
Rat.add.aux : ∀ (a b : ℚ) {g ad bd : ℕ},
  g = a.den.gcd b.den →
    ad = a.den / g →
      bd = b.den / g →
        have den := ad * b.den;
        have num := a.num * ↑bd + b.num * ↑ad;
        num.natAbs.gcd g = num.natAbs.gcd den
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Hom.cast_cast : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' u'' v'' : U} (e : u ⟶ v) (hu : u = u') (hv : v = v') (hu' : u' = u'')
  (hv' : v' = v''), Quiver.Hom.cast hu' hv' (Quiver.Hom.cast hu hv e) = Quiver.Hom.cast ⋯ ⋯ e
-- Mathlib.Topology.Algebra.Group.Basic
OrderDual.instIsTopologicalAddGroup : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G], IsTopologicalAddGroup Gᵒᵈ
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_zsmul_left : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute (↑u) a → ∀ (m : ℤ), AddCommute (↑(m • u)) a
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_int8ToBitVec : ∀ (x : Int8), Int64.ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instInhabited : (R : Type u) → [inst : Ring R] → Inhabited (ModuleCat R)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.insertIfNew : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β},
  ContinuousWithinAt g t (f x) → ContinuousWithinAt f s x → f ⁻¹' t ∈ nhdsWithin x s → ContinuousWithinAt (g ∘ f) s x
-- Lean.Parser.Command
Lean.Parser.Command.end.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The `j`-th column of a Young diagram consists of the cells whose second coordinate is `j`.  -/
YoungDiagram.col : YoungDiagram → ℕ → Finset (ℕ × ℕ)
-- Mathlib.GroupTheory.Coset.Basic
MonoidHom.fiberEquiv_symm_apply : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] (f : α →* H) (a b : α) (g : ↑(⇑f ⁻¹' {f b})),
  ↑((f.fiberEquiv a b).symm g) = a * (b⁻¹ * ↑g)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.instContinuousSMulSubtypeContinuousMapMemSubmoduleCoindV : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} {H : Type u_8} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V] [inst_9 : Group H]
  [inst_10 : TopologicalSpace H] (φ : G →ₜ* H) (π : ContRepresentation R G V),
  ContinuousSMul R ↥(ContRepresentation.coindV φ π)
-- Mathlib.Data.Nat.Find
Nat.findGreatest.congr_simp : ∀ (P P_1 : ℕ → Prop),
  P = P_1 →
    ∀ {inst : DecidablePred P} [inst_1 : DecidablePred P_1] (a a_1 : ℕ),
      a = a_1 → Nat.findGreatest P a = Nat.findGreatest P_1 a_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α},
  ∅.getKey? a = none
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_mul_relIndex : ∀ {G : Type u_1} [inst : AddGroup G] (H K L : AddSubgroup G), H ≤ K → K ≤ L → H.relIndex K * K.relIndex L = H.relIndex L
-- Mathlib.Algebra.Category.ModuleCat.Basic
LinearEquiv.toModuleIso_hom : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ : Type v} {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂} {m₁ : Module R X₁}
  {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂), e.toModuleIso.hom = ModuleCat.ofHom ↑e
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isOpenEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Topology.IsOpenEmbedding ⇑h
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⊥.dualAnnihilator = ⊤
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_eval : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R) (f : Polynomial R) (s : R),
  Polynomial.eval s ((Polynomial.taylor r) f) = Polynomial.eval (s + r) f