mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Regular.Basic
Commute.isRightRegular_iff : ∀ {R : Type u_1} [inst : Mul R] {a : R}, (∀ (b : R), Commute a b) → (IsRightRegular a ↔ IsLeftRegular a)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mul_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜] {f : α → 𝕜},
  MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (fun x => f x * c) μ
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (homGroup : autoParam ((P Q : C) → AddCommGroup (P ⟶ Q)) CategoryTheory.Preadditive.homGroup._autoParam) →
      autoParam
          (∀ (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R),
            CategoryTheory.CategoryStruct.comp (f + f') g =
              CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f' g)
          CategoryTheory.Preadditive.add_comp._autoParam →
        autoParam
            (∀ (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R),
              CategoryTheory.CategoryStruct.comp f (g + g') =
                CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f g')
            CategoryTheory.Preadditive.comp_add._autoParam →
          CategoryTheory.Preadditive C
-- Lean.Structure
_private.Lean.Structure.0.Lean.findParentProjStruct?.go : Lean.Environment → Lean.Name → Lean.Name → StateM Lean.NameSet (Option Lean.Name)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.trans_eventuallyEq : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f : α → E}
  {g₁ g₂ : α → F}, f =Θ[l] g₁ → g₁ =ᶠ[l] g₂ → f =Θ[l] g₂
-- Mathlib.Data.Part
Part.ofOption.eq_2 : ∀ {α : Type u_1} (a : α), ↑(some a) = Part.some a
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- The main part of `coherence` tactic.  -/
Mathlib.Tactic.Coherence.coherenceLoop : optParam ℕ 37 → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.UniformSpace.Cauchy
/-- Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function
defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that
is general enough to cover both ℕ and ℝ, which are the main motivating examples.  -/
CauchySeq : {α : Type u} → {β : Type v} → [uniformSpace : UniformSpace α] → [Preorder β] → (β → α) → Prop
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.getCollisionNodeSize : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.CollisionNode α β → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.isCycle_append : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u},
  p.IsPath → q.IsPath → p.support.tail.Disjoint q.support.tail → 1 < p.length ∨ 1 < q.length → (p.append q).IsCycle
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The range of a ring homomorphism, as a subfield of the target. See Note [range copy pattern].  -/
RingHom.fieldRange : {K : Type u} → {L : Type v} → [inst : DivisionRing K] → [inst_1 : DivisionRing L] → (K →+* L) → Subfield L
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- A simp theorem or information about a declaration to unfold by simp.
This is stored in the oleans to implement the `simp` attribute and user-defined simp sets.
 -/
Lean.Meta.SimpEntry : Type
-- Mathlib.Data.List.Forall2
List.forall₂_map_left_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {f : γ → α} {l : List γ} {u : List β},
  List.Forall₂ R (List.map f l) u ↔ List.Forall₂ (fun c b => R (f c) b) l u
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.op_inr : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q), b.op.inr = b.snd.op
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Sheaf.instIsLocallyInjectiveFunImageι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G),
  CategoryTheory.Sheaf.IsLocallyInjective (CategoryTheory.Sheaf.imageι f)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.norm_le_norm_of_nonneg_of_le : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  autoParam (0 ≤ a) CStarAlgebra.norm_le_norm_of_nonneg_of_le._auto_1 → a ≤ b → ‖a‖ ≤ ‖b‖
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
/-- [Stacks Tag 02UP](https://stacks.math.columbia.edu/tag/02UP) -/
AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsProper f] (y : ↥Y),
  (⇑f ⁻¹' {y}).Finite → ∃ V, y ∈ V ∧ AlgebraicGeometry.IsFinite (f ∣_ V)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The identity natural transformation is a based natural isomorphism.  -/
CategoryTheory.BasedNatIso.id : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} → (F : CategoryTheory.BasedFunctor 𝒳 𝒴) → F ≅ F
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  {hf₁ : F.relativelyRepresentable f₁} {f₂ : F.obj A₂ ⟶ X} {f₃ : F.obj A₃ ⟶ X}
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [F.Faithful] {Z : C}
  {φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃},
  φ = φ' ↔
    CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃) =
        CategoryTheory.CategoryStruct.comp φ' (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃) ∧
      CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃) =
          CategoryTheory.CategoryStruct.comp φ'
            (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃) ∧
        CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃) =
          CategoryTheory.CategoryStruct.comp φ' (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_g'_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).g' φ.τ₃ =
    h.g'
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.HasIndepIncrements.indepFun_eval_sub : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] [inst_2 : SubNegZeroMonoid E],
  ProbabilityTheory.HasIndepIncrements X P →
    ∀ {r s t : T}, r ≤ s → s ≤ t → (∀ᵐ (ω : Ω) ∂P, X r ω = 0) → ProbabilityTheory.IndepFun (X s) (X t - X s) P
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.hom_inv_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ≅ Y) (Z : C) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.inv Z) h) =
    h
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdxD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → (a : α) × β a → Sort u_3) (x : ℕ)
  (fallback : (a : α) × β a)
  (h_1 : (x : ℕ) → (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf x fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (n : ℕ) → (fallback : (a : α) × β a) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, x, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => h_1 x fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback => h_2 size k v l r n fallback) =
    h_1 x fallback
-- Mathlib.Algebra.FreeAlgebra
/-- Addition in `Pre R X` defined as `Pre.add`. Note: Used for notation only.  -/
FreeAlgebra.Pre.hasAdd : (R : Type u_1) → (X : Type u_2) → Add (FreeAlgebra.Pre R X)
-- Mathlib.Algebra.Ring.Defs
instMulZeroOneClassOfSemiring : {α : Type u} → [Semiring α] → MulZeroOneClass α
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasStrictDerivAt_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) [inst_3 : One F], HasStrictDerivAt 1 0 x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (n m : ℤ) (z : CochainComplex.HomComplex.Cochain F G n),
  CochainComplex.HomComplex.δ n m (-z) = -CochainComplex.HomComplex.δ n m z
-- Mathlib.Order.RelClasses
/-- **Alias** of `Prod.wellFoundedGT`. -/
Prod.wellFoundedGT' : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [WellFoundedGT α] [inst_2 : Preorder β] [WellFoundedGT β],
  WellFoundedGT (α × β)
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.instInhabitedEqnInfo.default : Lean.Elab.PartialFixpoint.EqnInfo
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.instHasColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasColimits C],
  CategoryTheory.Limits.HasColimits (CategoryTheory.Over X)
-- Mathlib.Data.List.SplitLengths
_private.Mathlib.Data.List.SplitLengths.0.List.splitLengths.match_1.splitter : {α : Type u_1} →
  (motive : List α × List α → Sort u_2) → (x : List α × List α) → ((x0 x1 : List α) → motive (x0, x1)) → motive x
-- Mathlib.RingTheory.Jacobson.Semiprimary
IsSimpleModule.jacobson_eq_bot : ∀ (R : Type u_1) (M : Type u_3) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M],
  Module.jacobson R M = ⊥
-- Std.Async.ContextAsync
/-- Runs two computations concurrently and returns the result of the first to complete. Each computation runs
in its own child context; when either completes, the other is cancelled immediately.
 -/
Std.Async.ContextAsync.race : {α : Type} →
  [Inhabited α] →
    Std.Async.ContextAsync α →
      Std.Async.ContextAsync α → optParam Task.Priority Task.Priority.default → Std.Async.ContextAsync α
-- Mathlib.Order.Sublattice
LatticeHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] (toSupHom toSupHom_1 : SupHom α β)
  (e_toSupHom : toSupHom = toSupHom_1)
  (map_inf' : ∀ (a b : α), toSupHom.toFun (a ⊓ b) = toSupHom.toFun a ⊓ toSupHom.toFun b),
  { toSupHom := toSupHom, map_inf' := map_inf' } = { toSupHom := toSupHom_1, map_inf' := ⋯ }
-- Mathlib.Algebra.Module.ULift
/-- The `R`-linear equivalence between `ULift M` and `M`.

This is a linear version of `AddEquiv.ulift`.  -/
ULift.moduleEquiv : {R : Type u} →
  {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → ULift.{w, v} M ≃ₗ[R] M
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_natCast : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : α → β} (n : ℕ), WithBot.map f ↑n = ↑(f ↑n)
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a bundled semigroup homomorphism `M₁ →ₙ* M₂` from a function `f` and a proof that it
belongs to the closure of the range of the coercion from `M₁ →ₙ* M₂` (or another type of bundled
homomorphisms that has a `MulHomClass` instance) to `M₁ → M₂`.  -/
mulHomOfMemClosureRangeCoe : {M₁ : Type u_6} →
  {M₂ : Type u_7} →
    [inst : TopologicalSpace M₂] →
      [T2Space M₂] →
        [inst_2 : Mul M₁] →
          [inst_3 : Mul M₂] →
            [ContinuousMul M₂] →
              {F : Type u_8} →
                [inst_5 : FunLike F M₁ M₂] →
                  [MulHomClass F M₁ M₂] → (f : M₁ → M₂) → f ∈ closure (Set.range fun f x => f x) → M₁ →ₙ* M₂
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ext_iff : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  {w w' : HNNExtension.NormalWord d}, w = w' ↔ w.head = w'.head ∧ w.toList = w'.toList
-- Mathlib.Data.List.Triplewise
List.Triplewise.imp : ∀ {α : Type u_1} {l : List α} {p q : α → α → α → Prop},
  (∀ {a b c : α}, p a b c → q a b c) → List.Triplewise p l → List.Triplewise q l
-- Mathlib.Topology.Order
TopologicalSpace.setOfPred_isOpen_injective : ∀ {α : Type u}, Function.Injective fun t => {s | IsOpen s}
-- Mathlib.Analysis.Calculus.TangentCone.Real
/-- If a subset of a real vector space contains a segment, then the direction of this
segment belongs to the tangent cone at its endpoints.  -/
mem_tangentConeAt_of_segment_subset : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousSMul ℝ E]
  {s : Set E} {x y : E}, segment ℝ x y ⊆ s → y - x ∈ tangentConeAt ℝ s x
-- Mathlib.Analysis.Calculus.Deriv.Comp
/-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative within a set
equal to the Fréchet derivative of `l` applied to the derivative of `f`.  -/
HasFDerivWithinAt.comp_hasDerivWithinAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E} {y : F} {t : Set F},
  HasFDerivWithinAt l l' t y →
    HasDerivWithinAt f f' s x → Set.MapsTo f s t → y = f x → HasDerivWithinAt (l ∘ f) (l' f') s x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_right_inj : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [IsRightCancelAdd α], z ≠ ⊥ → (x + z = y + z ↔ x = y)
-- Mathlib.RingTheory.Ideal.Basic
Ideal.span_single_eq_top : ∀ {ι : Type u_5} [inst : DecidableEq ι] [Finite ι] (R : ι → Type u_6) [inst_2 : (i : ι) → Semiring (R i)],
  Ideal.span (Set.range fun i => Pi.single i 1) = ⊤
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_of_add_le_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddRightMono α] {a b c d : α}, a + b ≤ c → d ≤ a → d + b ≤ c
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_natural_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y Y' : C}
  [inst_2 : CategoryTheory.Closed A] (f : X ⟶ A ⟹ Y) (g : Y ⟶ Y'),
  CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom A).map g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry f) g
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCriterion.existence : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.ValuativeCriterion f → AlgebraicGeometry.ValuativeCriterion.Existence f
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.instTensorProduct : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Algebra.IsStandardOpenImmersion R T],
  Algebra.IsStandardOpenImmersion S (TensorProduct R S T)
-- Mathlib.GroupTheory.Coset.Basic
AddMonoidHom.fiberEquivKer_symm_apply : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] (f : α →+ H) (a : α) (g : ↥f.ker),
  ↑((f.fiberEquivKer a).symm g) = a + ↑g
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The categorical product of rings is the Cartesian product of rings. This is its `Fan`.
 -/
CommRingCat.piFan : {ι : Type u} → (R : ι → CommRingCat) → CategoryTheory.Limits.Fan R
-- Init.MetaTypes
/-- Use "smart unfolding" when reducing definitions, to ensure the primitive recursors
are not exposed. Default: `false`.  -/
Lean.Meta.Command.ReduceConfig.smartUnfolding : Lean.Meta.Command.ReduceConfig → Bool
-- Mathlib.AlgebraicGeometry.Cover.Directed
CategoryTheory.Precoverage.ZeroHypercover.pullback₁.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C}
  [inst_1 : J.IsStableUnderBaseChange] (f f_1 : S ⟶ T) (e_f : f = f_1) (E E_1 : J.ZeroHypercover T) (e_E : E = E_1)
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)],
  CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E = CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f_1 E_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {km : α}, t.min! = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.inter : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
  {s t u : Set α}, Absorbs G₀ s u → Absorbs G₀ t u → Absorbs G₀ (s ∩ t) u
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- The base ring is a left identity for the tensor product of modules, up to linear equivalence.
 -/
TensorProduct.lid : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_5) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorProduct R R M ≃ₗ[R] M
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.beq_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap.Raw α β cmp} [inst : (k : α) → BEq (β k)]
  [inst_1 : Std.LawfulEqCmp cmp] [Std.TransCmp cmp] {m₃ m₄ : Std.DTreeMap.Raw α β cmp},
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → m₁.beq m₂ = m₃.beq m₄
-- Mathlib.CategoryTheory.Category.Preorder
OrderHom.equivFunctor_apply : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (f : X →o Y),
  OrderHom.equivFunctor f = f.toFunctor
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
Algebra.discr.eq_1 : ∀ {ι : Type w} [inst : DecidableEq ι] (A : Type u) {B : Type v} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Fintype ι] (b : ι → B), Algebra.discr A b = (Algebra.traceMatrix A b).det
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpIndSMul_add : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x y : G),
  MeasureTheory.condExpIndSMul hm hs hμs (x + y) =
    MeasureTheory.condExpIndSMul hm hs hμs x + MeasureTheory.condExpIndSMul hm hs hμs y
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.PComp.mk.injEq : ∀ (c : Mathlib.Tactic.Linarith.Comp) (src : Mathlib.Tactic.Linarith.CompSource)
  (history effective implicit vars : Std.TreeSet ℕ compare) (c_1 : Mathlib.Tactic.Linarith.Comp)
  (src_1 : Mathlib.Tactic.Linarith.CompSource) (history_1 effective_1 implicit_1 vars_1 : Std.TreeSet ℕ compare),
  ({ c := c, src := src, history := history, effective := effective, implicit := implicit, vars := vars } =
      { c := c_1, src := src_1, history := history_1, effective := effective_1, implicit := implicit_1,
        vars := vars_1 }) =
    (c = c_1 ∧ src = src_1 ∧ history = history_1 ∧ effective = effective_1 ∧ implicit = implicit_1 ∧ vars = vars_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.type₂_simplex : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι),
  (h.type₂ s).simplex =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (h.index s))) (h.simplex s)
-- Mathlib.Data.TypeVec
TypeVec.dropFun_prod : ∀ {n : ℕ} {α α' β β' : TypeVec.{u_1} (n + 1)} (f : α.Arrow β) (f' : α'.Arrow β'),
  TypeVec.dropFun (TypeVec.prod.map f f') = TypeVec.prod.map (TypeVec.dropFun f) (TypeVec.dropFun f')