mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.NormTrace
Algebra.norm_one_add_smul : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [Module.Free A B]
  [Module.Finite A B] (a : A) (x : B), ∃ r, (Algebra.norm A) (1 + a • x) = 1 + (Algebra.trace A B) x * a + r * a ^ 2
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_smul_root_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j k : ι),
  P.reflectionPerm i = P.reflectionPerm j → P.pairing k i • P.root i = P.pairing k j • P.root j
-- Init.Data.List.Attach
List.pmap.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f f_1 : (a : α) → P a → β),
  f = f_1 → ∀ (l l_1 : List α) (e_l : l = l_1) (H : ∀ a ∈ l, P a), List.pmap f l H = List.pmap f_1 l_1 ⋯
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Auxiliary construction to build a rotation by the oriented angle `θ`.  -/
Orientation.rotationAux : {V : Type u_1} →
  [inst : NormedAddCommGroup V] →
    [inst_1 : InnerProductSpace ℝ V] →
      [Fact (Module.finrank ℝ V = 2)] → Orientation ℝ V (Fin 2) → Real.Angle → V →ₗᵢ[ℝ] V
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link2.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r r' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + r.size) → Sort u_3) (ℓ : Std.DTreeMap.Internal.Impl α β)
  (hℓ₁ : ℓ.Balanced) (hℓ₂ : ℓ.size = r'.size + r.size)
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = r'.size + r.size) → motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }),
  (match { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } with
    | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) =
    h_1 ℓ hℓ₁ hℓ₂
-- Mathlib.Order.Fin.Basic
Fin.orderIsoSubtype_symm_apply : ∀ {n : ℕ} (a : { i // i < n }), (RelIso.symm Fin.orderIsoSubtype) a = ⟨↑a, ⋯⟩
-- Mathlib.Data.Sym.Basic
Sym.attach_nil : ∀ {α : Type u_1}, Sym.nil.attach = Sym.nil
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContDiffWithinAt.comp_contMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_6} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_7} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F']
  {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {s : Set M} {t : Set F} {x : M},
  ContDiffWithinAt 𝕜 n g t (f x) →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F) n f s x →
      s ⊆ f ⁻¹' t → ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) s x
-- Init.Data.BitVec.Lemmas
BitVec.clz.eq_1 : ∀ {w : ℕ} (x : BitVec w), x.clz = x.clzAuxRec (w - 1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul' : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [IsDomain k] [Module.IsTorsionFree k V] {p₁ q₁ p₂ q₂ : P},
  line[k, p₁, q₁].Parallel line[k, p₂, q₂] ↔ ∃ z, z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
-- Lean.Elab.InfoTree.Types
Lean.Elab.ContextInfo.mk : Lean.Elab.CommandContextInfo → Option Lean.Name → Array Lean.Expr → Lean.Elab.ContextInfo
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasStrictDerivAt_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (c : F), HasStrictDerivAt (fun x => c) 0 x
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Composition with a linear map before and after alternatization are equivalent.  -/
LinearMap.compMultilinearMap_alternatization : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} {N'₂ : Type u_10} [inst_5 : AddCommGroup N'₂]
  [inst_6 : Module R N'₂] [inst_7 : DecidableEq ι] [inst_8 : Fintype ι] (g : N' →ₗ[R] N'₂)
  (f : MultilinearMap R (fun x => M) N'),
  MultilinearMap.alternatization (g.compMultilinearMap f) = g.compAlternatingMap (MultilinearMap.alternatization f)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracket_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W W₁ : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt (T% W) x →
    MDiffAt (T% W₁) x →
      VectorField.mlieBracket I V (W + W₁) x = VectorField.mlieBracket I V W x + VectorField.mlieBracket I V W₁ x
-- Init.Data.List.Sublist
List.prefix_nil : ∀ {α : Type u_1} {l : List α}, l <+: [] ↔ l = []
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.open_target : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] (c : ChartedSpaceCore H M) {e : PartialEquiv M H},
  e ∈ c.atlas → IsOpen e.target
-- Lean.Compiler.Options
Lean.Compiler.compiler.traceUnnormalized : Lean.Option Bool
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.I₀ × 𝒰Y.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).f ij =
    CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰X.f ij.1) f)
      (CategoryTheory.CategoryStruct.comp (𝒰Y.f ij.2) g) f g (𝒰X.f ij.1) (𝒰Y.f ij.2)
      (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftAssocTensor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C × C × C),
  (CategoryTheory.MonoidalCategory.leftAssocTensor C).obj X =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 X.2.1) X.2.2
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections],
  GrpCat.limitCone F =
    CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ GrpCat MonCat)))
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.whiskerLeft_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] (X x x_1 : P.FullSubcategory) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.obj f.hom)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_filter_containsKey_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getEntry? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = none
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGT : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsLE X b],
  t.IsLE ((t.truncGT a).obj X) b
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.CollectState.visited : Lean.Meta.Grind.Action.CollectState✝ → Std.HashSet Lean.Meta.Sym.ExprPtr
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Module.Basis.constrL_basis : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] {ι : Type u_1} [inst_11 : Finite ι] [inst_12 : T2Space E]
  (v : Module.Basis ι 𝕜 E) (f : ι → F) (i : ι), (v.constrL f) (v i) = f i
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.of_tower : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [NumberField K] [NumberField L]
  [inst_4 : Algebra K L] (E : Type u_3) [inst_5 : Field E] [inst_6 : Algebra K E] [inst_7 : Algebra E L]
  [IsScalarTower K E L], NumberField E
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.shiftIso_add_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n m a a' a'' : A) (ha' : n + a = a')
  (ha'' : m + a' = a'') (X : C),
  (F.shiftIso (m + n) a a'' ⋯).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X))
        ((F.shiftIso n a a' ha').hom.app X))
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
exists_lt_of_lt_csSup' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α}, a < sSup s → ∃ b ∈ s, a < b
-- Mathlib.Data.Ordmap.Invariants
Ordnode.splitMin_eq : ∀ {α : Type u_1} (s : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α),
  l.splitMin' x r = (l.findMin' x, (Ordnode.node s l x r).eraseMin)
-- Mathlib.RingTheory.Flat.TorsionFree
/-- If every localization of `R` at a maximal ideal is a valuation ring then an `R`-module
is flat iff it has no torsion.  -/
Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsDomain R],
  (∀ (P : Ideal R) [inst_4 : P.IsMaximal], ValuationRing (Localization P.primeCompl)) →
    (Module.Flat R M ↔ Submodule.torsion R M = ⊥)
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.setOfIdeal_open : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [T2Space R] (I : Ideal C(X, R)), IsOpen (ContinuousMap.setOfIdeal I)
-- Mathlib.Computability.EpsilonNFA
εNFA.toNFA_evalFrom_match : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (start : Set σ), M.toNFA.evalFrom (M.εClosure start) = M.evalFrom start
-- Mathlib.Order.Filter.Defs
/-- The relative complement of two filters `f \ g` contains sets
whose union with any set in `g` lies in `f`.  -/
Filter.instSDiff : {α : Type u_1} → SDiff (Filter α)
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- If the map $M' \otimes N \to M \otimes N$ is injective for every finitely generated submodule
$M' \subseteq M$, then it is in fact injective for every submodule $M' \subseteq M$.  -/
TensorProduct.rTensor_injective_of_forall_fg_rTensor_injective : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N],
  (∀ (M' : Submodule R M), M'.FG → Function.Injective ⇑(LinearMap.rTensor N M'.subtype)) →
    ∀ (M' : Submodule R M), Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instZero : {X : AlgebraicGeometry.Scheme} → Zero X.IdealSheafData
-- Mathlib.Order.BooleanAlgebra.Set
/-- A version of `sdiff_union_sdiff_cancel` with more general hypotheses.  -/
Set.sdiff_union_sdiff_cancel' : ∀ {α : Type u_1} {s t u : Set α}, s ∩ u ⊆ t → t ⊆ s ∪ u → s \ t ∪ t \ u = s \ u
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The counit of an adjunction  -/
CategoryTheory.Adjunction.counit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} → (F ⊣ G) → (G.comp F ⟶ CategoryTheory.Functor.id D)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.exactPairingUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.ExactPairing (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.mk : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} →
      [inst_1 : Ring S] →
        [inst_2 : Algebra R S] →
          (toMulRingNorm : MulRingNorm S) →
            (∀ (a : R) (x : S), toMulRingNorm.toFun (a • x) = ‖a‖ * toMulRingNorm.toFun x) → MulAlgebraNorm R S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- Mathlib.CategoryTheory.Sites.InducedTopology
/-- Variant of `Functor.restrictedTopology_eq_inducedTopology` that is sometimes easier to use.  -/
CategoryTheory.Functor.restrictedTopology_eq_inducedTopology_of_isContinuous : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [F.IsContinuous J K], F.restrictedTopology K = J → F.inducedTopology K = J
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
/-- A morphism is "quasi-compact" if the underlying map of topological spaces is, i.e. if the preimages
of quasi-compact open sets are quasi-compact.
 -/
AlgebraicGeometry.QuasiCompact : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpan`
if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `R` such that
`P` holds for `Rᵣ →+* Sᵣ`.

Note that this is equivalent to `RingHom.OfLocalizationFiniteSpan` via
`RingHom.ofLocalizationSpan_iff_finite`, but this has less restrictions when applying.  -/
RingHom.OfLocalizationSpan : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Analysis.Convex.Segment
segment_translate_image : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (a b c : E), (fun x => a + x) '' segment 𝕜 b c = segment 𝕜 (a + b) (a + c)
-- Mathlib.Data.Sum.Interval
Finset.inr_mem_sumLift₂ : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f : α₁ → β₁ → Finset γ₁} {g : α₂ → β₂ → Finset γ₂} {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂} {c₂ : γ₂},
  Sum.inr c₂ ∈ Finset.sumLift₂ f g a b ↔ ∃ a₂ b₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ c₂ ∈ g a₂ b₂
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.coe_multisetSum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (c : AddCon M) (s : Multiset ι) (f : ι → M),
  ↑(Multiset.map f s).sum = (Multiset.map (fun i => ↑(f i)) s).sum
-- Mathlib.Data.Prod.Basic
Prod.mk_left_inj : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β}, (a₁, b) = (a₂, b) ↔ a₁ = a₂
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.adjoin_nonUnitalSubalgebra_eq_span : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (s : NonUnitalSubalgebra R A), Subalgebra.toSubmodule (Algebra.adjoin R ↑s) = R ∙ 1 ⊔ s.toSubmodule
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
/-- An additive subgroup `H` of `G` determines an additive subgroup
`H.op` of the opposite additive group `Gᵃᵒᵖ`.  -/
AddSubgroup.opEquiv : {G : Type u_2} → [inst : AddGroup G] → AddSubgroup G ≃o AddSubgroup Gᵃᵒᵖ
-- Mathlib.Combinatorics.Graph.Basic
Graph.mem_loopSet : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) (e : β), e ∈ Graph.loopSet x ↔ G.IsLoopAt e x
-- Init.Data.Vector.Monadic
_private.Init.Data.Vector.Monadic.0.Array.forIn'_eq_foldlM.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (b : ForInStep β) → ((b : β) → motive (ForInStep.yield b)) → ((b : β) → motive (ForInStep.done b)) → motive b
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, analyticOrderAt (-f) z₀ = analyticOrderAt f z₀
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio.size : Lean.Elab.HoverableInfoPrio → ℕ
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.apply_ind : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M)
  (hx : x ∈ s), ↑(fs.toFun (fs.ind x hx)) x = 1
-- Mathlib.Tactic.DeprecateTo
/-- If the input command is a `theorem` or a `lemma`, then it replaces the name of the
resulting declaration with `newName` and it returns the old declaration name and the
command with the new name.

If the input command is neither a `theorem` nor a `lemma`, then it returns
`.missing` and the unchanged command.
 -/
Mathlib.Tactic.DeprecateTo.renameTheorem : Lean.TSyntax `ident → Lean.TSyntax `command → Lean.TSyntax `Lean.Parser.Command.declId × Lean.TSyntax `command
-- Lean.Meta.SynthInstance
/-- Try to synthesize metavariable `mvar` using the instance `inst`.
Remark: `mctx` is set using `withMCtx`.
If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
A subgoal is created for each instance implicit parameter of `inst`.  -/
Lean.Meta.SynthInstance.tryResolve : Lean.Expr → Lean.Meta.SynthInstance.Instance → Lean.MetaM (Option (Lean.MetavarContext × List Lean.Expr))
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_sub : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (x y : MonoidAlgebra R M), (x - y).coeff = x.coeff - y.coeff
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mk.inj : ∀ {X : AlgebraicGeometry.Scheme} {ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))}
  {map_ideal_basicOpen :
    ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) =
        ideal (X.affineBasicOpen f)}
  {supportSet : Set ↥X}
  {supportSet_eq_iInter_zeroLocus :
    autoParam (supportSet = ⋂ U, X.zeroLocus ↑(ideal U))
      AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus._autoParam}
  {ideal_1 : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))}
  {map_ideal_basicOpen_1 :
    ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal_1 U) =
        ideal_1 (X.affineBasicOpen f)}
  {supportSet_1 : Set ↥X}
  {supportSet_eq_iInter_zeroLocus_1 :
    autoParam (supportSet_1 = ⋂ U, X.zeroLocus ↑(ideal_1 U))
      AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus._autoParam},
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet := supportSet,
        supportSet_eq_iInter_zeroLocus := supportSet_eq_iInter_zeroLocus } =
      { ideal := ideal_1, map_ideal_basicOpen := map_ideal_basicOpen_1, supportSet := supportSet_1,
        supportSet_eq_iInter_zeroLocus := supportSet_eq_iInter_zeroLocus_1 } →
    ideal = ideal_1 ∧ supportSet = supportSet_1
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The isomorphism between `completeBipartiteGraph V₁ W₁` and
`completeBipartiteGraph V₂ W₂` where `V₁ ≃ V₂` and `W₁ ≃ W₂`.  -/
SimpleGraph.completeBipartiteGraphCongr : {V₁ : Type u_5} →
  {V₂ : Type u_6} →
    {W₁ : Type u_7} → {W₂ : Type u_8} → V₁ ≃ V₂ → W₁ ≃ W₂ → completeBipartiteGraph V₁ W₁ ≃g completeBipartiteGraph V₂ W₂
-- Mathlib.Algebra.Order.Interval.Basic
Interval.length_nonneg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (s : Interval α), 0 ≤ s.length
-- Mathlib.Topology.Order.LiminfLimsup
Monotone.limsup_nhdsGT_eq_iInf₂ : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [DenselyOrdered α] [inst_4 : CompleteLattice β] {f : α → β} [NoMaxOrder α],
  Monotone f → ∀ (a : α), Filter.limsup f (nhdsWithin a (Set.Ioi a)) = ⨅ r, ⨅ (_ : r > a), f r
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_map_smul : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [BorelSpace E] (r : ℝ) (t : E),
  MeasureTheory.charFun (MeasureTheory.Measure.map (fun x => r • x) μ) t = MeasureTheory.charFun μ (r • t)
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- The subcomplex generated by a simplex.  -/
SSet.S.subcomplex : {X : SSet} → X.S → X.Subcomplex
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_one : ↑1 = 1
-- Batteries.Data.BitVec.Lemmas
BitVec.toNat_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool), (BitVec.ofFnBE f).toNat = Nat.ofBits (f ∘ Fin.rev)
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.instIsLeftKanExtensionIdInvRightUnitorOfIsDense : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsDense], (CategoryTheory.Functor.id D).IsLeftKanExtension F.rightUnitor.inv
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.d.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (a a_1 : ℕ) (h_1 : (n m : ℕ) → motive (Int.ofNat n) (Int.ofNat m))
  (h_2 : (n m : ℕ) → motive (Int.negSucc n) (Int.negSucc m)) (h_3 : Unit → motive (Int.negSucc 0) (Int.ofNat 0))
  (h_4 : (a a_2 : ℕ) → motive (Int.ofNat a) (Int.negSucc a_2))
  (h_5 : (a a_2 : ℕ) → motive (Int.negSucc a) (Int.ofNat a_2)),
  (match Int.ofNat a, Int.negSucc a_1 with
    | Int.ofNat n, Int.ofNat m => h_1 n m
    | Int.negSucc n, Int.negSucc m => h_2 n m
    | Int.negSucc 0, Int.ofNat 0 => h_3 ()
    | Int.ofNat a, Int.negSucc a_2 => h_4 a a_2
    | Int.negSucc a, Int.ofNat a_2 => h_5 a a_2) =
    h_4 a a_1
-- Mathlib.NumberTheory.FunctionField
/-- Let `K` be a function field over `F`. If `E` is an algebraic extension of `F` which is
contained in `K` then it is finite over `F`.  -/
FunctionField.instFiniteDimensionalSubtypeMemIntermediateFieldOfIsAlgebraic : ∀ {F : Type u_1} (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : FaithfulSMul (Polynomial F) K] [FunctionField F K] [inst_5 : Algebra F K] (E : IntermediateField F K)
  [inst_6 : Algebra (Polynomial ↥E) K] [FaithfulSMul (Polynomial ↥E) K] [IsScalarTower (Polynomial F) (Polynomial ↥E) K]
  [Algebra.IsAlgebraic F ↥E], FiniteDimensional F ↥E
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, IsUnit a → IsUnit b → IsUnit (a * b)