mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Discriminant
/-- Let `K` be the fraction field of an integrally closed domain `R` and let `L` be a finite
separable extension of `K`. Let `B : PowerBasis K L` be such that `IsIntegral R B.gen`.
Then for all, `z : L` that are integral over `R`, we have
`(discr K B.basis) • z ∈ adjoin R ({B.gen} : Set L)`.  -/
Algebra.discr_mul_isIntegral_mem_adjoin : ∀ (K : Type u) {L : Type v} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Module.Finite K L] {R : Type z}
  [inst_4 : CommRing R] [inst_5 : Algebra R K] [inst_6 : Algebra R L] [IsScalarTower R K L] [Algebra.IsSeparable K L]
  [IsIntegrallyClosed R] [IsFractionRing R K] {B : PowerBasis K L},
  IsIntegral R B.gen → ∀ {z : L}, IsIntegral R z → Algebra.discr K ⇑B.basis • z ∈ R[B.gen]
-- Mathlib.Topology.Sets.VietorisTopology
Topology.IsClosedEmbedding.compacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsClosedEmbedding f), Topology.IsClosedEmbedding (TopologicalSpace.Compacts.map f ⋯)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.coe_lTensor_symm : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N ≃ₗ[R] P), ↑(LinearEquiv.lTensor M f).symm = LinearMap.lTensor M ↑f.symm
-- Mathlib.Topology.UniformSpace.Defs
/-- A uniform embedding is injective.  -/
IsUniformEmbedding.injective : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformEmbedding f → Function.Injective f
-- Mathlib.RingTheory.PowerBasis
PowerBasis.exists_smodEq : ∀ {A : Type u_4} {B : Type u_5} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (pb : PowerBasis A B)
  (b : B), ∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.ExactAt.op : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K : HomologicalComplex V c} {i : ι}, K.ExactAt i → K.op.ExactAt i
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The linear map from the group of continuous maps from `α` to `β` to the group of equivalence
classes of `μ`-almost-everywhere measurable functions.  -/
ContinuousMap.toAEEqFunLinearMap : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      (μ : MeasureTheory.Measure α) →
        [inst_1 : TopologicalSpace α] →
          [BorelSpace α] →
            {𝕜 : Type u_5} →
              [inst_3 : Semiring 𝕜] →
                [inst_4 : TopologicalSpace γ] →
                  [TopologicalSpace.PseudoMetrizableSpace γ] →
                    [inst_6 : AddCommGroup γ] →
                      [inst_7 : Module 𝕜 γ] →
                        [inst_8 : IsTopologicalAddGroup γ] →
                          [inst_9 : ContinuousConstSMul 𝕜 γ] →
                            [SecondCountableTopologyEither α γ] → C(α, γ) →ₗ[𝕜] α →ₘ[μ] γ
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)),
  AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P =
    CategoryTheory.CategoryStruct.comp
      ((AlgebraicTopology.DoldKan.N₂.comp AlgebraicTopology.DoldKan.Γ₂).map P.decompId_i)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.hom
              AlgebraicTopology.DoldKan.Γ₂N₁.natTrans).app
          P.X)
        P.decompId_p)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Fintype.prod_eq_prod_compl_mul : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (a : ι) (f : ι → M),
  ∏ i, f i = (∏ i ∈ {a}ᶜ, f i) * f a
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.fill.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor)
  (parent : RBTree.RBNode.Path α) (y : α) (b a : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a)
  (h_3 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b),
  (match RBTree.RBNode.Path.left c parent y b, a with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left c parent y b, a => h_2 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b => h_3 c a y parent b) =
    h_2 c parent y b a
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The product of `x y : R[M]` is the finitely supported function whose value at `m`
is the sum of `x m₁ * y m₂` over all pairs `m₁, m₂` such that `m₁ + m₂ = m`.  -/
AddMonoidAlgebra.instMul : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Add M] → Mul (AddMonoidAlgebra R M)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S T : 𝒮} {a b c : 𝒳} (f : R ⟶ S) (g : S ⟶ T) (φ : a ⟶ b) (ψ : b ⟶ c)
  [p.IsHomLift f φ] [p.IsHomLift g ψ],
  p.IsHomLift (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.mem_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → (k ∈ t₁ ↔ k ∈ t₂)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_inv_hom_hom_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.typesWith_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : (L.withConstants α).Sentence),
  T.typesWith (FirstOrder.Language.BoundedFormula.not φ) = (T.typesWith φ)ᶜ
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (u : Rˣ) (r s t : R),
  sizeOf { u := u, r := r, s := s, t := t } = 1 + sizeOf u + sizeOf r + sizeOf s + sizeOf t
-- Mathlib.Order.Basic
eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt : ∀ {α : Type u_2} [inst : LinearOrder α] {x y x' y' : α}, (x < y ↔ x' < y') → (y < x ↔ y' < x') → (x = y ↔ x' = y')
-- Batteries.Data.List.Basic
List.all₂.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Bool) (x : List α) (x_1 : List β),
  (x = [] → x_1 = [] → False) →
    (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_1 = b :: bs → False) → List.all₂ r x x_1 = false
-- Mathlib.Data.Multiset.Replicate
/-- **Alias** of the reverse direction of `Multiset.eq_replicate_card`. -/
Multiset.eq_replicate_of_mem : ∀ {α : Type u_1} {a : α} {s : Multiset α}, (∀ b ∈ s, b = a) → s = Multiset.replicate s.card a
-- Mathlib.Topology.MetricSpace.Gluing
Metric.inductiveLimitDist.eq_1 : ∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] (f : (n : ℕ) → X n → X (n + 1)) (x y : (n : ℕ) × X n),
  Metric.inductiveLimitDist f x y = dist (Nat.leRecOn ⋯ (fun {k} => f k) x.snd) (Nat.leRecOn ⋯ (fun {k} => f k) y.snd)
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Given homomorphisms `f : G →g G'` and `g : H →g H'`, returns a homomorphism from `G ⊕g H` to
`G' ⊕g H'` that applies `f` to the left component and `g` to the right component.  -/
SimpleGraph.Hom.sum : {V : Type u_3} →
  {V' : Type u_4} →
    {W : Type u_5} →
      {W' : Type u_6} →
        {G : SimpleGraph V} →
          {H : SimpleGraph W} → {G' : SimpleGraph V'} → {H' : SimpleGraph W'} → G →g G' → H →g H' → G ⊕g H →g G' ⊕g H'
-- Init.Data.List.Sort.Lemmas
List.mem_merge_right : ∀ {α : Type u_1} {r : List α} {x : α} {l : List α} (s : α → α → Bool), x ∈ r → x ∈ l.merge r s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE?.go.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a)) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGE?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryGE?.go k (some ⟨k', v⟩) l
    | Ordering.eq => some ⟨k', v⟩
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryGE?.go k best r
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage.eq_1 : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X),
  Dynamics.coverEntropyEntourage T F U = ExpGrowth.expGrowthSup fun n => ↑(Dynamics.coverMincard T F U n)
-- Init.Data.List.Sublist
List.suffix_cons : ∀ {α : Type u_1} (a : α) (l : List α), l <:+ a :: l
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.List.take.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) →
        ((x : List α) → motive 0 x) →
          ((n : ℕ) → motive n.succ []) → ((n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)) → motive x x_1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`, version subtracting vectors.  -/
Orientation.oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))
-- Lean.SubExpr
Lean.SubExpr.Pos.instDecidableEq : DecidableEq Lean.SubExpr.Pos
-- Init.Data.Ord.Vector
Vector.instReflOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.ReflOrd α] {n : ℕ}, Std.ReflOrd (Vector α n)
-- Mathlib.Topology.Category.Compactum
Compactum.instFaithfulForget : Compactum.forget.Faithful
-- Std.Data.DTreeMap.Internal.Balancing
/-- Precondition for `balanceLErase`. As Breitner et al. remark, "not very educational".  -/
Std.DTreeMap.Internal.Impl.BalanceLErasePrecond : ℕ → ℕ → Prop
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
tprod_eq_of_filter_le : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  {L₁ L₂ : SummationFilter β} [L₁.NeBot],
  L₁.filter ≤ L₂.filter → Multipliable f L₂ → ∏'[L₁] (b : β), f b = ∏'[L₂] (b : β), f b
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.map_intCast : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (z : ℤ), v ↑z = ‖z‖
-- Mathlib.GroupTheory.OrderOfElement
Prod.addOrderOf : ∀ {α : Type u_4} {β : Type u_5} [inst : AddMonoid α] [inst_1 : AddMonoid β] (x : α × β),
  addOrderOf x = (addOrderOf x.1).lcm (addOrderOf x.2)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_biUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {p : Filter ι} {s : Set γ} {S : γ → Set α},
  (∀ i ∈ s, IsOpen (S i)) →
    (∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i)) → TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i)
-- Mathlib.Order.Hom.Lattice
SupHom.instOrderTop : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → [OrderTop β] → OrderTop (SupHom α β)
-- Lean.Elab.MutualDef
/-- The error name for "failed to infer definition type" errors.

We cannot use `logNamedError` here because the error is logged later, after attempting to synthesize
metavariables, in `logUnassignedUsingErrorInfos`.
 -/
Lean.Elab.Term.failedToInferDefTypeErrorName : Lean.Name
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromTarget.instIsomorphismsOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms], P.InheritedFromTarget (CategoryTheory.MorphismProperty.isomorphisms C)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X i ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV 𝒰 f g i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f i))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
        ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i)) h)
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalSkip : Lean.Elab.Tactic.Tactic
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.sum_mult_mul_log : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ),
  ∑ w, ↑w.mult * Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x)) = 0
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.eq_snd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X}
  (F : f₀.HomotopyRel f₁ S) (t : ↑unitInterval) {x : X}, x ∈ S → F (t, x) = f₁ x
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_sub_add_eq_sub_left : ∀ {a b c : ENNReal}, autoParam (c ≠ ⊤) ENNReal.add_sub_add_eq_sub_left._auto_1 → c + a - (c + b) = a - b
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.smul_of_top_left : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [IsBoundedSMul 𝕜 β] {f : α → β} {φ : α → 𝕜},
  MeasureTheory.Integrable φ μ → MeasureTheory.MemLp f ⊤ μ → MeasureTheory.Integrable (φ • f) μ
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_singleton_ssubset`. -/
Set.diff_singleton_ssubset : ∀ {α : Type u_1} {s : Set α} {a : α}, s \ {a} ⊂ s ↔ a ∈ s
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.leftHomologyData_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.leftHomologyData.H = 0
-- Mathlib.Order.BooleanSubalgebra
/-- The natural lattice hom from a Boolean subalgebra to the original lattice.  -/
BooleanSubalgebra.subtype : {α : Type u_2} → [inst : BooleanAlgebra α] → (L : BooleanSubalgebra α) → BoundedLatticeHom (↥L) α
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.image_eq_preimage_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (S : Set A), ⇑e '' S = ⇑e.symm ⁻¹' S
-- Mathlib.Topology.Bases
TopologicalSpace.nonempty_of_mem_countableBasis : ∀ {α : Type u} [t : TopologicalSpace α] [inst : SecondCountableTopology α] {s : Set α},
  s ∈ TopologicalSpace.countableBasis α → s.Nonempty
-- Mathlib.Algebra.Order.Star.Basic
star_mul_self_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  (r : R), 0 ≤ star r * r
-- Batteries.Recycling.RBTree.WF
/-- Sufficient condition for `map` to preserve an `All` quantifier.  -/
RBTree.RBNode.All.map : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {q : β → Prop} {f : α → β},
  (∀ {x : α}, p x → q (f x)) →
    ∀ {t : RBTree.RBNode α}, RBTree.RBNode.All p t → RBTree.RBNode.All q (RBTree.RBNode.map f t)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.union_ae_eq_right_of_ae_eq_empty : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s =ᵐ[μ] ∅ → s ∪ t =ᵐ[μ] t
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.norm_inl : ∀ {R : Type u_3} {M : Type u_4} [inst : SeminormedRing R] [inst_1 : SeminormedAddCommGroup M] (r : R),
  ‖TrivSqZeroExt.inl r‖ = ‖r‖
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.mk.injEq : ∀ (tree : Lean.Meta.DiscrTree Aesop.RulePatternIndex.Entry) (isEmpty : Bool)
  (tree_1 : Lean.Meta.DiscrTree Aesop.RulePatternIndex.Entry) (isEmpty_1 : Bool),
  ({ tree := tree, isEmpty := isEmpty } = { tree := tree_1, isEmpty := isEmpty_1 }) =
    (tree = tree_1 ∧ isEmpty = isEmpty_1)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.Literal.mk.sizeOf_spec : ∀ (n : ℕ) (value : BitVec n), sizeOf { n := n, value := value } = 1 + sizeOf n + sizeOf value
-- Init.Control.Basic
ToBool : Type u → Type u
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.Ordering.swap.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.sub : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f g : α → G}
  [MeasurableSub₂ G], Measurable f → Measurable g → Measurable (f - g)
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Mon.mul : Nat.Internal.SOM.Mon → Nat.Internal.SOM.Mon → Nat.Internal.SOM.Mon
-- Mathlib.FieldTheory.Perfect
/-- Variant with `· ^ p` inside of `frobeniusEquiv`.  -/
frobeniusEquiv_symm_pow : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (frobeniusEquiv R p).symm (x ^ p) = x
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.instCategory.eq_1 : AddSemigrp.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := AddHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @AddSemigrp.instCategory._proof_1,
    comp_id := @AddSemigrp.instCategory._proof_2, assoc := @AddSemigrp.instCategory._proof_3 }
-- Mathlib.LinearAlgebra.Basis.Exact
/-- Let `0 → K → M → P → 0` be a split exact sequence of `R`-modules, let `s : M → K` be a
retraction of `f` and `v` be a basis of `M` indexed by `κ ⊕ σ`. Then
if `s vᵢ = 0` for `i : κ` and `(s vⱼ)ⱼ` is linear independent for `j : σ`, then
the images of `vᵢ` for `i : κ` form a basis of `P`.

For convenience this is stated for an arbitrary type `ι` with two maps `κ → ι` and `σ → ι`.  -/
Module.Basis.ofSplitExact : {R : Type u_1} →
  {M : Type u_2} →
    {K : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup K] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R K] →
                    [inst_6 : Module R P] →
                      {f : K →ₗ[R] M} →
                        {g : M →ₗ[R] P} →
                          {s : M →ₗ[R] K} →
                            s ∘ₗ f = LinearMap.id →
                              Function.Exact ⇑f ⇑g →
                                {ι : Type u_5} →
                                  {κ : Type u_6} →
                                    {σ : Type u_7} →
                                      {a : κ → ι} →
                                        {b : σ → ι} →
                                          Function.Surjective ⇑g →
                                            (v : Module.Basis ι R M) →
                                              Function.Injective a →
                                                (∀ (i : κ), s (v (a i)) = 0) →
                                                  LinearIndependent R (⇑s ∘ ⇑v ∘ b) →
                                                    Codisjoint (Set.range a) (Set.range b) → Module.Basis κ R P
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_zero : ∀ {w n acc : ℕ}, (0#w).cpopNatRec n acc = acc
-- Mathlib.Algebra.Order.Chebyshev
/-- **Chebyshev's Sum Inequality**: When `f` and `g` antivary together (e.g. one is monotone, the
other is antitone), the scalar product of their sum is less than the size of the set times their
scalar product.  -/
Antivary.card_smul_sum_le_sum_smul_sum : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Antivary f g → Fintype.card ι • ∑ i, f i • g i ≤ (∑ i, f i) • ∑ i, g i
-- Mathlib.Algebra.CharP.Defs
CharP.cast_eq_zero : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p], ↑p = 0
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMin'.eq_2 : ∀ {α : Type u_1} (x : α) (size : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α),
  (Ordnode.node size l x_2 r).findMin' x = l.findMin' x_2
-- Mathlib.Algebra.Module.Presentation.DirectSum
/-- Given an `A`-module `N` and a family `relations : ι → Relations A`,
the data of a solution of `Relations.directSum relations` in `N`
is equivalent to the data of a family of solutions of `relations i` in `N`
for all `i`.  -/
Module.Relations.Solution.directSumEquiv : {A : Type u} →
  [inst : Ring A] →
    {ι : Type w} →
      {relations : ι → Module.Relations A} →
        {N : Type v} →
          [inst_1 : AddCommGroup N] →
            [inst_2 : Module A N] →
              (Module.Relations.directSum relations).Solution N ≃ ((i : ι) → (relations i).Solution N)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.instPartialOrder : {ι : Type u_1} → PartialOrder (BoxIntegral.Box ι)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_le_cons : ∀ {α : Type u_1} {s t : Multiset α} (a : α), s ≤ t → a ::ₘ s ≤ a ::ₘ t
-- Batteries.Data.BinomialHeap.Basic
/-- `O(1)`. Make a new empty binomial heap.  -/
Batteries.BinomialHeap.empty : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le
-- Mathlib.Topology.Order
Equiv.induced_symm : ∀ {α : Type u_4} {β : Type u_5} (e : α ≃ β), TopologicalSpace.induced ⇑e.symm = TopologicalSpace.coinduced ⇑e
-- Mathlib.CategoryTheory.Action.Monoidal
Action.tensorUnit_V : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action V G)).V = CategoryTheory.MonoidalCategoryStruct.tensorUnit V
-- Init.Grind.Lemmas
Lean.Grind.Semiring.mul_zero_congr : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] {a b : α}, b = 0 → a * b = 0