mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
LinearMap.clmOfExistsBoundedImage_apply : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E]
  [inst_2 : IsTopologicalAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : TopologicalSpace F]
  [inst_5 : NontriviallyNormedField 𝕜] [inst_6 : Module 𝕜 E] [inst_7 : ContinuousSMul 𝕜 E] [inst_8 : NormedField 𝕜']
  [inst_9 : Module 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_10 : RingHomIsometric σ] [inst_11 : IsTopologicalAddGroup F]
  {f : E →ₛₗ[σ] F} {h : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V)} {x : E},
  (f.clmOfExistsBoundedImage h) x = f x
-- Std.Sat.AIG.Basic
Std.Sat.AIG.TernaryInput.rhs : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.TernaryInput → aig.Ref
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The projection map is surjective.  -/
GroupExtension.rightHom_surjective : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (self : GroupExtension N E G), Function.Surjective ⇑self.rightHom
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionSemiHomClass.mk : ∀ {F : Type u_8} {M : outParam (Type u_9)} {N : outParam (Type u_10)} {φ : outParam (M → N)} {X : outParam (Type u_11)}
  {Y : outParam (Type u_12)} [inst : SMul M X] [inst_1 : SMul N Y] [inst_2 : FunLike F X Y],
  (∀ (f : F) (c : M) (x : X), f (c • x) = φ c • f x) → MulActionSemiHomClass F φ X Y
-- Lean.Meta.WHNF
/-- Retrieves `ConstInfo` for `declName`.
Remark: if `ignoreTransparency = false`, then `getUnfoldableConst?` is used.
For example, if `ignoreTransparency = false` and `transparencyMode = .reducible` and `declName` is not reducible,
then the result is `none`.
 -/
_private.Lean.Meta.WHNF.0.Lean.Meta.getConstInfo? : Lean.Name → Bool → Lean.MetaM (Option Lean.ConstantInfo)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.revAll_prop_eq_revAll_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.revAll p = s.revAll fun x => decide (p x)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.continuous_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_3} [inst_1 : TopologicalSpace Y] (f : OnePoint X → Y),
  Continuous f ↔
    Filter.Tendsto (fun x => f ↑x) (Filter.coclosedCompact X) (nhds (f OnePoint.infty)) ∧ Continuous fun x => f ↑x
-- Lean.Log
/-- Log a new error message using the given message data. The position is provided by `getRef`.  -/
Lean.logError : {m : Type → Type} →
  [Monad m] → [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.MessageData → m Unit
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The ideal `J ⊓ I` is a sub-dp-ideal of `I` if and only if the divided powers have
some compatibility mod `J`. (The necessity was proved as a sanity check.)  -/
DividedPowers.isSubDPIdeal_inf_iff : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A},
  hI.IsSubDPIdeal (J ⊓ I) ↔ ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
-- Mathlib.Algebra.Star.Basic
star_inv₀ : ∀ {R : Type u} [inst : GroupWithZero R] [inst_1 : StarMul R] (x : R), star x⁻¹ = (star x)⁻¹
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  {X Y : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A} (f : X ⟶ Y) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).functor.map f).hom.app X_1 =
    f.hom.app (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.term_one : ∀ {n : ℕ}, 0 < n → ZetaAsymptotics.term n 1 = Real.log (↑n + 1) - Real.log ↑n - 1 / (↑n + 1)
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_mkSlice_roi : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = (Std.Slice.toArray xs).extract (lo + 1)
-- Lean.Widget.Commands
Lean.Widget.widgetInstanceSpec : Lean.ParserDescr
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_closure_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X
-- Mathlib.Data.Fin.Pigeonhole
/-- If we have a surjective map from `Fin m` to `Fin n`, then `m ≥ n`.
See also `Fintype.card_le_of_surjective` for the generalisation to arbitrary finite types.
 -/
Fin.le_of_surjective : ∀ {m n : ℕ} (f : Fin m → Fin n), Function.Surjective f → n ≤ m
-- Mathlib.Data.List.Induction
_private.Mathlib.Data.List.Induction.0.List.bidirectionalRec.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (h_1 : Unit → motive []) (h_2 : (a : α) → motive [a])
  (h_3 : (a b : α) → (l : List α) → motive (a :: b :: l)),
  (match [a] with
    | [] => h_1 ()
    | [a] => h_2 a
    | a :: b :: l => h_3 a b l) =
    h_2 a
-- Aesop.Forward.RuleInfo
/-- The number of distinct level parameters and level metavariables occurring
in the rule's type. We expect that these turn into level metavariables when
the rule is elaborated.  -/
Aesop.ForwardRuleInfo.numLevelParams : Aesop.ForwardRuleInfo → ℕ
-- Init.Data.List.Lemmas
List.all_congr : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ = l₂ → ∀ {p q : α → Bool}, (∀ (a : α), p a = q a) → l₁.all p = l₂.all q
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.currNamespace : Lean.Elab.CommandContextInfo → Lean.Name
-- Mathlib.Analysis.Convex.Hull
convexHull_convexHull_union_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s t : Set E), (convexHull 𝕜) ((convexHull 𝕜) s ∪ t) = (convexHull 𝕜) (s ∪ t)
-- Lean.Compiler.ExternAttr
Lean.instBEqExternAttrData : BEq Lean.ExternAttrData
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.zero : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S), WittVector.mapFun (⇑f) 0 = 0
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.Node.injEq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (a : Option β)
  (a_1 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) (a_2 : Option β)
  (a_3 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp),
  (Lean.PrefixTreeNode.Node a a_1 = Lean.PrefixTreeNode.Node a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- An additive subgroup `K` includes `closure k` if and only if it includes `k`  -/
AddSubgroup.closure_le : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {k : Set G}, AddSubgroup.closure k ≤ K ↔ k ⊆ ↑K
-- Init.Data.Range.Polymorphic.PRange
/-- `*...b` is the range of elements less than `b`. See also `Std.Rio`.  -/
Std.«term*..._» : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.isPlausibleIndirectOutput_of_mem_toList : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β} {b : β},
  b ∈ it.toList → it.IsPlausibleIndirectOutput b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_getElem?_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.ExtTreeMap α β cmp}, t₁ = t₂ ↔ ∀ (k : α), t₁[k]? = t₂[k]?
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
_private.Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing.0.ModularForm.E₄CubeSubE₆SqForm.eq_1 : ModularForm.E₄CubeSubE₆SqForm✝ =
  ModularForm.mcast ModularForm.E₄CubeSubE₆SqForm._proof_1✝ (ModularForm.E₄.pow 3)
      ModularForm.E₄CubeSubE₆SqForm._proof_3✝ -
    ModularForm.mcast ModularForm.E₄CubeSubE₆SqForm._proof_4✝ (ModularForm.E₆.pow 2)
      ModularForm.E₄CubeSubE₆SqForm._proof_3✝
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_self : ∀ {G : Type u_1} [inst : Group G] (g : G), ⁅g, g⁆ = 1
-- Mathlib.Control.Basic
seq_map_assoc : ∀ {α β γ : Type u} {F : Type u → Type v} [inst : Applicative F] [LawfulApplicative F] (x : F (α → β)) (f : γ → α)
  (y : F γ), x <*> f <$> y = (fun x => x ∘ f) <$> x <*> y
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_add_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {f g : AddMonoidAlgebra R A},
  AddMonoidAlgebra.supDegree D (f + g) ≤ AddMonoidAlgebra.supDegree D f ⊔ AddMonoidAlgebra.supDegree D g
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.rank.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.rank K = Fintype.card (NumberField.InfinitePlace K) - 1
-- Mathlib.Algebra.Module.PID
/-- A finitely generated torsion module over a PID is an internal direct sum of its
`p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`.  -/
Submodule.isInternal_prime_power_torsion_of_pid : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : IsDomain R] [Module.Finite R M],
  Module.IsTorsion R M →
    DirectSum.IsInternal fun p =>
      Submodule.torsionBy R M
        (Submodule.IsPrincipal.generator ↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.hasse_adj : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (SimpleGraph.hasse α).Adj a b ↔ a ⋖ b ∨ b ⋖ a
-- Mathlib.Data.List.Intervals
List.Ico.bagInter_consecutive : ∀ (n m l : ℕ), (List.Ico n m).bagInter (List.Ico m l) = []
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- The Kronecker tensor product. This is just a shorthand for `kroneckerMap (⊗ₜ)`.
Prefer the notation `⊗ₖₜ` rather than this definition.  -/
Matrix.kroneckerTMul : (R : Type u_1) →
  {α : Type u_3} →
    {β : Type u_5} →
      {l : Type u_9} →
        {m : Type u_10} →
          {n : Type u_11} →
            {p : Type u_12} →
              [inst : CommSemiring R] →
                [inst_1 : AddCommMonoid α] →
                  [inst_2 : AddCommMonoid β] →
                    [inst_3 : Module R α] →
                      [inst_4 : Module R β] → Matrix l m α → Matrix n p β → Matrix (l × n) (m × p) (TensorProduct R α β)
-- Mathlib.Data.Fintype.Order
Finite.exists_ge : ∀ {ι : Sort u_1} {α : Type u_2} [Finite ι] [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] (f : ι → α),
  ∃ M, ∀ (i : ι), M ≤ f i
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_add_one : ∀ {a : ByteArray} {i : ℕ} (ha : i + 1 ≤ a.size), a.extract i (i + 1) = [a[i]].toByteArray
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.isDiameter_ninePointCircle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.ninePointCircle.IsDiameter (s.faceOppositeCentroid i) (s.eulerPoint i)
-- Mathlib.Topology.Sets.VietorisTopology
Topology.IsEmbedding.nonemptyCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsEmbedding f), Topology.IsEmbedding (TopologicalSpace.NonemptyCompacts.map f ⋯)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_Iio : ∀ {m n : ℕ} (h : m = n) (i : Fin n), Fin.cast h ⁻¹' Set.Iio i = Set.Iio (Fin.cast ⋯ i)
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.mkDerivationₗ_X : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] (f : σ → A) (i : σ), (MvPolynomial.mkDerivationₗ R f) (MvPolynomial.X i) = f i
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.extFunctorObj_obj_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) (n : ℕ) (Y : C),
  ↑((CategoryTheory.Abelian.extFunctorObj X n).obj Y) = CategoryTheory.Abelian.Ext X Y n
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_of_indep_of_le_left : ∀ {Ω : Type u_1} {m₁ m₂ m₃ _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.Indep m₁ m₂ μ → m₃ ≤ m₁ → ProbabilityTheory.Indep m₃ m₂ μ
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.toUpper_le_toUpper : ∀ {α : Type u_1} [inst : Preorder α] {x y : α}, Topology.WithUpper.toUpper x ≤ Topology.WithUpper.toUpper y ↔ x ≤ y
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_ssubset_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ⊂ Set.Ici b ↔ b < a
-- Mathlib.CategoryTheory.Category.Cat.Terminal
/-- The discrete category on `PUnit` is terminal.  -/
CategoryTheory.Cat.isTerminalDiscretePUnit : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of (CategoryTheory.Discrete PUnit.{u_1 + 1}))
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toRingHom_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'),
  (e₁.trans e₂).toRingHom = e₂.toRingHom.comp e₁.toRingHom
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loopless_iff_forall_not_isLoop : ∀ {α : Type u_1} {M : Matroid α}, M.Loopless ↔ ∀ e ∈ M.E, ¬M.IsLoop e
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.instPartialOrder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : CategoryTheory.Functor C MonCat} → PartialOrder (CategoryTheory.SubmonoidFunctor M)
-- Mathlib.Data.ZMod.Basic
ZMod.lift_injective : ∀ (n : ℕ) {A : Type u_2} [inst : AddGroup A] {f : { f // f ↑n = 0 }},
  Function.Injective ⇑((ZMod.lift n) f) ↔ ∀ (m : ℤ), ↑f m = 0 → ↑m = 0
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.instPreadditive : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → CategoryTheory.Preadditive (HomologicalComplex V c)
-- Mathlib.CategoryTheory.SmallObject.Basic
CategoryTheory.MorphismProperty.HasSmallObjectArgument.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : CategoryTheory.MorphismProperty C},
  (∃ κ, ∃ (x : Fact κ.IsRegular), ∃ x_1, I.IsCardinalForSmallObjectArgument κ) → I.HasSmallObjectArgument
-- Mathlib.RingTheory.Ideal.Defs
Ideal.ext : ∀ {α : Type u} [inst : Semiring α] {I J : Ideal α}, (∀ (x : α), x ∈ I ↔ x ∈ J) → I = J
-- Mathlib.Order.Hom.WithTopBot
OrderEmbedding.withTopMap_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β), ⇑f.withTopMap = WithTop.map ⇑f
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x))
      (CategoryTheory.CategoryStruct.comp (Y.fromSpecResidueField (f x)) h) =
    CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.rfl : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.IsInducedSubgraph G
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.range_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection], (↑U.starProjection).range = U
-- Mathlib.Data.Finset.Empty
Finset.exists_mem_empty_iff : ∀ {α : Type u_1} (p : α → Prop), (∃ x ∈ ∅, p x) ↔ False
-- Mathlib.FieldTheory.Galois.Basic
/-- See `InfiniteGalois.mem_bot_iff_fixed` for the infinite case,
i.e. without the `[FiniteDimensional F E]` assumption.  -/
IsGalois.mem_bot_iff_fixed : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [IsGalois F E]
  [FiniteDimensional F E] (x : E), x ∈ ⊥ ↔ ∀ (f : Gal(E/F)), f x = x
-- Init.Data.UInt.Lemmas
UInt16.toUSize_add : ∀ (a b : UInt16), (a + b).toUSize = (a.toUSize + b.toUSize) % 65536
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.smul_absolutelyContinuous : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {c : ENNReal}, (c • μ).AbsolutelyContinuous μ
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Coyoneda.objOpOp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (X_1 : Cᵒᵖ),
  (CategoryTheory.Coyoneda.objOpOp X).inv.app X_1 = (CategoryTheory.opEquiv (Opposite.op X) X_1).toIso.inv
-- Mathlib.Algebra.Star.Basic
eq_star_iff_eq_star : ∀ {R : Type u} [inst : InvolutiveStar R] {r s : R}, r = star s ↔ s = star r
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_hom₂ : ∀ {ι : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid O] (s : Multiset ι) (f : M → N → O),
  (∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d) →
    f 0 0 = 0 →
      ∀ (f₁ : ι → M) (f₂ : ι → N),
        (Multiset.map (fun i => f (f₁ i) (f₂ i)) s).sum = f (Multiset.map f₁ s).sum (Multiset.map f₂ s).sum
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.ker_comapₗ : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : TopologicalSpace Y] {Z : Type u_6}
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid Z] [inst_4 : Module R Z] (f : C(X, Y)),
  Function.Surjective ⇑f → (LocallyConstant.comapₗ R f).ker = ⊥
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι)
  (π₀ : BoxIntegral.Prepartition I),
  (BoxIntegral.IntegrationParams.toFilteriUnion I π₀).HasBasis (fun r => ∀ (c : NNReal), l.RCond (r c)) fun r =>
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}
-- Mathlib.Algebra.Group.Prod
Prod.instIsMulTorsionFree : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] [IsMulTorsionFree M] [IsMulTorsionFree N],
  IsMulTorsionFree (M × N)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_sdiff_loops_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.closure (X \ M.loops) = M.closure X
-- Mathlib.Tactic.Widget.SelectInsertParamsClass
/-- Handler deriving a `SelectInsertParamsClass` instance.  -/
Lean.Elab.mkSelectInsertParamsInstanceHandler : Array Lean.Name → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE_refl : ∀ {X : Type u} [inst : Preorder X] {x : X} (h : x ≤ x), h.hom = CategoryTheory.CategoryStruct.id x
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.congr_apply_right : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂)
  (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) (x : N₁ ⋊[φ₁] G₁),
  ((SemidirectProduct.congr fn fg h) x).right = fg x.right
-- Mathlib.Data.Rat.Init
NNRat.cast_eq_id : NNRat.cast = id
-- Lean.Meta.Tactic.Grind.Action
/-- A terminal action which closes the goal or not.
This kind of action may make progress, but we only include `mkTac` into the resulting tactic sequence
if it closed the goal.
 -/
Lean.Meta.Grind.Action.terminalAction : Lean.Meta.Grind.GoalM Bool → Lean.Meta.Grind.GrindM Lean.Meta.Grind.TGrind → Lean.Meta.Grind.Action
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_smul_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ),
  ProbabilityTheory.covariance (c • X) Y μ = c * ProbabilityTheory.covariance X Y μ
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- Note that this does not apply to a non-unital ring, with counterexample where the elementwise
congruence relation `!![⊤,⊤;⊤,(· ≡ · [PMOD 4])]` is a ring congruence over
`Matrix (Fin 2) (Fin 2) 2ℤ`.  -/
RingCon.matrix_ofMatrix : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (c : RingCon (Matrix n n R)), RingCon.matrix n c.ofMatrix = c
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.coe_mapLinearMap : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [inst_7 : CategoryTheory.Functor.Linear R F] [inst_8 : F.Additive] {X Y : C},
  ⇑(CategoryTheory.Functor.mapLinearMap R F) = F.map
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
/-- If `C` has strict terminal objects and `X` is a terminal object, the category
`Under X` is equivalent to a point.  -/
CategoryTheory.underEquivOfIsTerminal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasStrictTerminalObjects C] →
      (X : C) → CategoryTheory.Limits.IsTerminal X → (CategoryTheory.Under X ≌ CategoryTheory.Discrete PUnit.{w + 1})
-- Mathlib.Data.Set.Function
Set.LeftInvOn.rightInvOn_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f' : β → α},
  Set.LeftInvOn f' f s → Set.RightInvOn f' f (f '' s)
-- Lean.Server.Requests
Lean.Server.RequestM.mapTaskCostly : {α : Type u_1} →
  {β : Type} →
    Lean.Server.ServerTask α → (α → Lean.Server.RequestM β) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D Eᵒᵖ) (X : Cᵒᵖ),
  (F.leftOpComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.unop X))))
-- Mathlib.RingTheory.LocalProperties.Projective
instProjectiveLocalizationAlgebraMapSubmonoid : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Module.Projective R A], Module.Projective (Localization S) (Localization (Algebra.algebraMapSubmonoid A S))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Variant of `homMk'` where both objects are applications of `mk`.  -/
CategoryTheory.StructuredArrow.mkPostcomp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {Y Y' : C} →
            {T : CategoryTheory.Functor C D} →
              (f : S ⟶ T.obj Y) →
                (g : Y ⟶ Y') →
                  CategoryTheory.StructuredArrow.mk f ⟶
                    CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f (T.map g))
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- A cyclotomic finite extension of a number field is a number field.  -/
IsCyclotomicExtension.numberField : ∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [h : NumberField K]
  [Finite ↑S] [IsCyclotomicExtension S K L], NumberField L
-- Mathlib.Data.Finset.Grade
/-- **Alias** of the reverse direction of `Finset.val_covBy_val`. -/
CovBy.finset_val : ∀ {α : Type u_1} {s t : Finset α}, s ⋖ t → s.val ⋖ t.val
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.subsingleton_of_isMulCommutative : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsPerfect G] [h_comm : IsMulCommutative G], Subsingleton G
-- Lean.Elab.Term.TermElabM
/-- Map from user name to internal unique name  -/
Lean.Elab.Term.Context.sectionVars : Lean.Elab.Term.Context → Lean.NameMap Lean.Name