mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Gcd
Int.lcm_pos : ∀ {m n : ℤ}, m ≠ 0 → n ≠ 0 → 0 < m.lcm n
-- Mathlib.Control.Functor.Multivariate
TypeVec.RelLast.eq_1 : ∀ {n : ℕ} (α : TypeVec.{u} n) {β γ : Type u} (r : β → γ → Prop) (i : Fin2 n), α.RelLast r = Eq
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instIsOrderedAddMonoid : ∀ {α : Type u_1} {x : MeasurableSpace α}, IsOrderedAddMonoid (MeasureTheory.Measure α)
-- Std.Time.Date.Basic
/-- Convert `Second.Offset` into `Week.Offset`.
 -/
Std.Time.Second.Offset.toWeeks : Std.Time.Second.Offset → Std.Time.Week.Offset
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.add_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f g : M →ₗ⁅R,L⁆ N) (m : M), (f + g) m = f m + g m
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_sub_left_right_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime x (x * z - y) ↔ IsCoprime x y
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- A function `f` is differentiable at `conj z` iff `star ∘ f ∘ conj` is differentiable at `z`.  -/
differentiableAt_star_conj_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {x : 𝕜} [NormedStarGroup 𝕜]
  {f : 𝕜 → F}, DifferentiableAt 𝕜 (star ∘ f ∘ ⇑(starRingEnd 𝕜)) x ↔ DifferentiableAt 𝕜 f ((starRingEnd 𝕜) x)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- generator of `F⟮α⟯`  -/
IntermediateField.AdjoinSimple.gen : (F : Type u_1) → [inst : Field F] → {E : Type u_2} → [inst_1 : Field E] → [inst_2 : Algebra F E] → (α : E) → ↥F⟮α⟯
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T T' : AlgebraicGeometry.Scheme.Pullback.Triplet f g}
  (h : T = T'),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr h).hom) T.SpecTensorTo =
    T'.SpecTensorTo
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.NormalizedHom.nil.inj : ∀ {e : Mathlib.Tactic.BicategoryLike.Mor₁} {a : Mathlib.Tactic.BicategoryLike.Obj}
  {e_1 : Mathlib.Tactic.BicategoryLike.Mor₁} {a_1 : Mathlib.Tactic.BicategoryLike.Obj},
  Mathlib.Tactic.BicategoryLike.NormalizedHom.nil e a = Mathlib.Tactic.BicategoryLike.NormalizedHom.nil e_1 a_1 →
    e = e_1 ∧ a = a_1
-- Mathlib.Probability.Martingale.Upcrossing
/-- `lowerCrossingTimeAux a f c N` is the first time `f` reached below `a` after time `c` before
time `N`.  -/
MeasureTheory.lowerCrossingTimeAux : {Ω : Type u_1} → {ι : Type u_2} → [Preorder ι] → [InfSet ι] → ℝ → (ι → Ω → ℝ) → ι → ι → Ω → ι
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.mul_prod_Ioi_eq_prod_Ici : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrderTop α] (a : α), f a * ∏ x > a, f x = ∏ x ≥ a, f x
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjObj.hom_ext : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] {Z : C} {f g : Z ⟶ W.weightedLimObjObj F},
  (∀ {j : J} (x : W.obj j),
      CategoryTheory.CategoryStruct.comp f (W.weightedLimObjObjπ F x) =
        CategoryTheory.CategoryStruct.comp g (W.weightedLimObjObjπ F x)) →
    f = g
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.toReal_essSup : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  (∀ᵐ (a : α) ∂μ, f a ≠ ⊤) →
    (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) fun i => (f i).toReal) →
      (essSup f μ).toReal = essSup (fun a => (f a).toReal) μ
-- Init.Data.Iterators.PostconditionMonad
/-- Converts an operation from `PostConditionT m` to `m`, discarding the postcondition.
 -/
Std.Iterators.PostconditionT.run : {m : Type w → Type w'} → [Monad m] → {α : Type w} → Std.Iterators.PostconditionT m α → m α
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) {M : Type w'} [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [inst_5 : L.IsLocalization W]
  [inst_6 : L.CommShift M] {X Y : C} [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m₀ : M)
  (hm₀ : m₀ = 0) (f : X ⟶ Y),
  (CategoryTheory.Localization.SmallShiftedHom.equiv W L) (CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f) =
    CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (L.map f)
-- Mathlib.Logic.Equiv.Basic
/-- For a fixed function `x₀ : {a // p a} → β` defined on a subtype of `α`,
the subtype of functions `x : α → β` that agree with `x₀` on the subtype `{a // p a}`
is naturally equivalent to the type of functions `{a // ¬ p a} → β`.  -/
Equiv.subtypePreimage : {α : Sort u_1} →
  {β : Sort u_4} →
    (p : α → Prop) → [DecidablePred p] → (x₀ : { a // p a } → β) → { x // x ∘ Subtype.val = x₀ } ≃ ({ a // ¬p a } → β)
-- Init.Data.Vector.Count
Vector.countP_pos_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, 0 < Vector.countP p xs ↔ ∃ a ∈ xs, p a = true
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.clm_comp : ∀ {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₂] [inst_1 : Semiring R₃] {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4}
  {M₂ : Type u_5} {M₃ : Type u_6} [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : TopologicalSpace M₃] [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂]
  [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₃ M₃] {f : M₁ → M₂},
  IsCompactOperator f → ∀ (g : M₂ →SL[σ₂₃] M₃), IsCompactOperator (⇑g ∘ f)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.succ_preAleph : ∀ (o : Ordinal.{u_1}), Order.succ (Cardinal.preAleph o) = Cardinal.preAleph (o + 1)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.Monic.eq_X_add_C : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → p.natDegree = 1 → p = Polynomial.X + Polynomial.C (p.coeff 0)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.instFintypeZero : {α : Type u_2} → [inst : Zero α] → Fintype ↑0
-- Mathlib.Data.NNReal.Defs
NNReal.coe_pow : ∀ (r : NNReal) (n : ℕ), ↑(r ^ n) = ↑r ^ n
-- Mathlib.Data.Set.Lattice
Set.Ici_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), Set.Ici (sSup s) = ⋂ a ∈ s, Set.Ici a
-- Mathlib.Data.Set.Lattice.Image
Set.monotone_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Monotone (Set.preimage f)
-- Init.Grind.Config
Lean.Grind.instInhabitedConfig.default : Lean.Grind.Config
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.abs_sin_eq_one_iff : ∀ {x : ℝ}, |Real.sin x| = 1 ↔ ∃ k, Real.pi / 2 + ↑k * Real.pi = x
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm_eq_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeAddGroup α}, x.norm = 0 ↔ x = 0
-- Mathlib.Topology.Order.IsLUB
Dense.exists_seq_strictMono_tendsto_of_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [FirstCountableTopology α] {s : Set α},
  Dense s →
    ∀ {x y : α}, y < x → ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo y x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalExprConfig_1.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.RingNF.Config
-- Mathlib.Algebra.Lie.BaseChange
_private.Mathlib.Algebra.Lie.BaseChange.0.LieAlgebra.ExtendScalars.bracket_lie_self : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (x : TensorProduct R A L), ⁅x, x⁆ = 0
-- Init.Data.String.Lemmas.Basic
String.Pos.nextn_toSlice : ∀ {n : ℕ} {s : String} {p : s.Pos}, p.toSlice.nextn n = (p.nextn n).toSlice
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂).getKey k h' = m₂.getKey k ⋯
-- Mathlib.RingTheory.Polynomial.HilbertPoly
/-- `Polynomial.hilbertPoly p 0 = 0`; for any `d : ℕ`, `Polynomial.hilbertPoly p (d + 1)`
is defined as `∑ i ∈ p.support, (p.coeff i) • Polynomial.preHilbertPoly F d i`. If
`M` is a graded module whose Poincaré series can be written as `p(X)/(1 - X)ᵈ` for some
`p : ℚ[X]` with integer coefficients, then `Polynomial.hilbertPoly p d` is the Hilbert
polynomial of `M`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval`,
which says that `PowerSeries.coeff F n (p * PowerSeries.invOneSubPow F d)` equals
`(Polynomial.hilbertPoly p d).eval (n : F)` for any large enough `n : ℕ`.
 -/
Polynomial.hilbertPoly : {F : Type u_1} → [inst : Field F] → Polynomial F → ℕ → Polynomial F
-- Mathlib.Data.Finite.Prod
Set.Infinite.image2_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} {a : α},
  t.Infinite → a ∈ s → Set.InjOn (f a) t → (Set.image2 f s t).Infinite
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_keq_cert.eq_1 : ∀ (lhs rhs : Lean.Grind.CommRing.Expr) (k : ℤ) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.imp_keq_cert lhs rhs k p₁ p₂ =
    (!k.beq' 0).and' (((lhs.sub rhs).toPoly_k.beq' p₁).and' (p₂.beq' (Lean.Grind.CommRing.Poly.num 0)))
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (toPseudofunctor : CategoryTheory.Pseudofunctor B C)
  (map_id :
    autoParam
      (∀ (X : B),
        toPseudofunctor.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toPseudofunctor.obj X))
      CategoryTheory.StrictlyUnitaryPseudofunctor.map_id._autoParam)
  (mapId_eq_eqToIso :
    autoParam (∀ (X : B), toPseudofunctor.mapId X = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso._autoParam)
  (toPseudofunctor_1 : CategoryTheory.Pseudofunctor B C)
  (map_id_1 :
    autoParam
      (∀ (X : B),
        toPseudofunctor_1.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toPseudofunctor_1.obj X))
      CategoryTheory.StrictlyUnitaryPseudofunctor.map_id._autoParam)
  (mapId_eq_eqToIso_1 :
    autoParam (∀ (X : B), toPseudofunctor_1.mapId X = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso._autoParam),
  ({ toPseudofunctor := toPseudofunctor, map_id := map_id, mapId_eq_eqToIso := mapId_eq_eqToIso } =
      { toPseudofunctor := toPseudofunctor_1, map_id := map_id_1, mapId_eq_eqToIso := mapId_eq_eqToIso_1 }) =
    (toPseudofunctor = toPseudofunctor_1)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.le_degrees_add_left : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  Disjoint p.degrees q.degrees → p.degrees ≤ (p + q).degrees
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Three points are affinely independent if and only if they are not collinear.  -/
affineIndependent_iff_not_collinear_set : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k {p₁, p₂, p₃}
-- Mathlib.Analysis.Complex.Circle
Circle.instCoeOut : CoeOut Circle ℂ
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.lt_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LT ι] [inst_2 : (i : ι) → LT (α i)]
  {a b : Colex (Π₀ (i : ι), α i)},
  a < b ↔ ∃ i, (∀ (j : ι), i < j → (ofColex a) j = (ofColex b) j) ∧ (ofColex a) i < (ofColex b) i
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictSupport_eq_span : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R] (s : Set (σ →₀ ℕ)),
  MvPolynomial.restrictSupport R s = Submodule.span R ((fun x => (MvPolynomial.monomial x) 1) '' s)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_subset_Iic_union_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio b ⊆ Set.Iic a ∪ Set.Ioo a b
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
AbsoluteValue.comp.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : Semiring T] [inst_1 : Semiring R] [inst_2 : Semiring S]
  [inst_3 : PartialOrder S] (v v_1 : AbsoluteValue R S),
  v = v_1 → ∀ {f f_1 : T →+* R} (e_f : f = f_1) (hf : Function.Injective ⇑f), v.comp hf = v_1.comp ⋯
-- Mathlib.Order.Filter.Pointwise
Filter.div_le_div_left : ∀ {α : Type u_2} [inst : Div α] {f g₁ g₂ : Filter α}, g₁ ≤ g₂ → f / g₁ ≤ f / g₂
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.erase : Lean.Meta.FVarSubst → Lean.FVarId → Lean.Meta.FVarSubst
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.const_eq : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] [MeasurableSingletonClass β]
  {f : α → β}, Measurable f → ∀ (a : β), Measurable fun x => a = f x
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k).get? a = if (k == a) = true then none else m.get? a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cycles_ext_iff : ∀ {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] {A : C} (f₁ f₂ : A ⟶ S.cycles),
  f₁ = f₂ ↔ CategoryTheory.CategoryStruct.comp f₁ S.iCycles = CategoryTheory.CategoryStruct.comp f₂ S.iCycles
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.dist_toSnowflaking_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : Dist X] (x y : X),
  dist (Metric.Snowflaking.toSnowflaking x) (Metric.Snowflaking.toSnowflaking y) = dist x y ^ α
-- Aesop.Frontend.Tactic
Aesop.Frontend.Parser.ruleSetSpec : Lean.ParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] (f : ι → β → α) (g : β → α) (s : Set β)
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasSumLocallyUniformlyOn f g s = TendstoLocallyUniformlyOn (fun x1 x2 => ∑ i ∈ x1, f i x2) g Filter.atTop s
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.instTypeNameRealizeValueResult : TypeName Lean.Meta.RealizeValueResult✝
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_le_subst_nonpos : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_le_subst_nonpos_cert x p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ = 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Init.Data.Option.Attach
Option.attach_map_subtype_val : ∀ {α : Type u_1} (o : Option α), Option.map Subtype.val o.attach = o
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.min?.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (c : RBTree.RBColor) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c RBTree.RBNode.nil v r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (l = RBTree.RBNode.nil → False) →
    (match RBTree.RBNode.node c l v r with
      | RBTree.RBNode.nil => h_1 ()
      | RBTree.RBNode.node c RBTree.RBNode.nil v r => h_2 c v r
      | RBTree.RBNode.node c l v r => h_3 c l v r) =
      h_3 c l v r
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_map_hom : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] (L : List ι) (f : ι → M)
  {G : Type u_8} [inst_2 : FunLike G M N] [AddMonoidHomClass G M N] (g : G),
  (List.map (⇑g ∘ f) L).sum = g (List.map f L).sum
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_eq_refl : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (i : A),
  CategoryTheory.shiftFunctorComm C i i =
    CategoryTheory.Iso.refl ((CategoryTheory.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C i))
-- Init.Data.SInt.Basic
instXorOpInt8 : XorOp Int8
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.slash_apply : ∀ {k : ℤ} (f : UpperHalfPlane → ℂ) (g : GL (Fin 2) ℝ) (τ : UpperHalfPlane),
  SlashAction.map k g f τ =
    (UpperHalfPlane.σ g) (f (g • τ)) * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) *
      UpperHalfPlane.denom g ↑τ ^ (-k)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.mulVecBilin_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : SMulCommClass S R A]
  [inst_6 : SMulCommClass S A A] [inst_7 : IsScalarTower R A A] [inst_8 : Fintype n] (M : Matrix m n A) (v : n → A),
  ((Matrix.mulVecBilin R S) M) v = M.mulVec v
-- Mathlib.Probability.Moments.CovarianceBilinDual
StrongDual.toLp.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) (p : ENNReal)
  [inst_4 : Fact (1 ≤ p)], StrongDual.toLp μ p = StrongDual.toLp μ p
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearEquiv_ridIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  (TensorProduct.ridIsometry 𝕜 E).toLinearEquiv = TensorProduct.rid 𝕜 E
-- Mathlib.CategoryTheory.Limits.Preorder
/-- If a partial order has binary products, then it is an inf-semilattice  -/
Preorder.semilatticeInfOfHasBinaryProducts : (C : Type u) → [inst : PartialOrder C] → [CategoryTheory.Limits.HasBinaryProducts C] → SemilatticeInf C
-- Init.Data.SInt.Lemmas
Int64.toUInt64_add : ∀ (a b : Int64), (a + b).toUInt64 = a.toUInt64 + b.toUInt64
-- Mathlib.Order.Hom.WithTopBot
SupHom.withBot_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (f : SupHom α β) (a : WithBot α),
  f.withBot a = WithBot.map (⇑f) a
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.comp_I : ∀ (J : Type u_1) [inst : LinearOrder J] {i j k : CategoryTheory.SimplicialThickening J}
  (f : CategoryTheory.SimplicialThickening.Path i.as j.as) (g : CategoryTheory.SimplicialThickening.Path j.as k.as),
  (CategoryTheory.CategoryStruct.comp f g).I = f.I ∪ g.I
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMinEntry?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → Std.DTreeMap.Const.minEntry? t₁ = Std.DTreeMap.Const.minEntry? t₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, t.isEmpty = (t.size == 0)
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.div_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ f₁ i) → (∀ i ∈ s, 0 < f₂ i) → MonovaryOn f₁ g s → AntivaryOn f₂ g s → MonovaryOn (f₁ / f₂) g s
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.apply_neg_self`. -/
AddAut.apply_inv_self : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M) (m : M), e ((-e) m) = m
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
EReal.measurableSpace : MeasurableSpace EReal
-- Lean.Meta.Tactic.Intro
/-- Introduce `n` binders in the goal `mvarId`.
 -/
Lean.MVarId.introN : Lean.MVarId → ℕ → optParam (List Lean.Name) [] → optParam Bool false → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- "iff" version of `Summable.of_nat_of_neg`.  -/
summable_int_iff_summable_nat_and_neg : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] {f : ℤ → G},
  Summable f ↔ (Summable fun n => f ↑n) ∧ Summable fun n => f (-↑n)
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If `f` is a function strictly monotone on a right neighborhood of `a` and the
image of this neighborhood under `f` meets every interval `(f a, b]`, `b > f a`, then `f` is
continuous at `a` from the right.

The assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` is required because otherwise the
function `f : ℝ → ℝ` given by `f x = if x ≤ 0 then x else x + 1` would be a counter-example at
`a = 0`.  -/
StrictMonoOn.continuousWithinAt_right_of_exists_between : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α},
  StrictMonoOn f s →
    s ∈ nhdsWithin a (Set.Ici a) → (∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b) → ContinuousWithinAt f (Set.Ici a) a
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Std.Internal.Do.EStateM.wpInst.match_1.splitter : {ε σ α : Type} →
  (motive : EStateM.Result ε σ α → Sort u_1) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → motive (EStateM.Result.ok a s')) →
        ((el : ε) → (s' : σ) → motive (EStateM.Result.error el s')) → motive x
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.id_f₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  (CategoryTheory.CategoryStruct.id S).f₀ = CategoryTheory.CategoryStruct.id S.L₀
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.inv_hom_id_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cocone F} (f : c ≅ d) {Z : C} (h : d.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.inv.hom (CategoryTheory.CategoryStruct.comp f.hom.hom h) = h
-- Aesop.RuleTac.ElabRuleTerm
Aesop.elabRuleTermForSimpMetaM : Lean.MVarId →
  Lean.Term →
    Lean.Meta.Simp.Context →
      Lean.Meta.Simp.SimprocsArray → Bool → Lean.MetaM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The isomorphism `toHoCat ⋙ toLocalization L ≅ ι ⋙ L` which expresses that
if `L : C ⥤ D` is a localization functor, then its restriction on the
full subcategory of cofibrant objects factors through the homotopy category
of cofibrant objects.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.toHoCatCompToLocalizationIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (L : CategoryTheory.Functor C D) →
            [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              HomotopicalAlgebra.CofibrantObject.toHoCat.comp
                  (HomotopicalAlgebra.CofibrantObject.HoCat.toLocalization L) ≅
                HomotopicalAlgebra.CofibrantObject.ι.comp L