mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dimension.Free
Module.nonempty_algEquiv_iff_finrank_eq_one : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [StrongRankCondition R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [Module.Free R S], Nonempty (R ≃ₐ[R] S) ↔ Module.finrank R S = 1
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.zsmul_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x : L}, x ∈ S → ∀ (n : ℤ), n • x ∈ S
-- Mathlib.RingTheory.Ideal.Maps
Ideal.instIsPrincipalIdealRingForallOfFinite : ∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] [Finite ι]
  [∀ (i : ι), IsPrincipalIdealRing (R i)], IsPrincipalIdealRing ((i : ι) → R i)
-- Lean.Meta.Transform
Lean.TransformStep.continue.injEq : ∀ (e? e?_1 : Option Lean.Expr), (Lean.TransformStep.continue e? = Lean.TransformStep.continue e?_1) = (e? = e?_1)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_split_dvd : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (k : ℕ) (b : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_right_split ctx p₁ p₂ k →
    Int.Internal.Linear.cooper_right_split_dvd_cert p₂ p' b ↑k = true → b ∣ Int.Internal.Linear.Poly.denote' ctx p'
-- Mathlib.Tactic.CongrExclamation
CongrState.mk.injEq : ∀ (goals : Array Lean.MVarId) (patterns : List (Lean.TSyntax `rintroPat)) (goals_1 : Array Lean.MVarId)
  (patterns_1 : List (Lean.TSyntax `rintroPat)),
  ({ goals := goals, patterns := patterns } = { goals := goals_1, patterns := patterns_1 }) =
    (goals = goals_1 ∧ patterns = patterns_1)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.im_coe : ∀ (z : Complex.UnitClosedDisc), (↑z).im = z.im
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α},
  k ∉ m₁ → Std.ExtDHashMap.Const.get! (m₁.union m₂) k = Std.ExtDHashMap.Const.get! m₂ k
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.annotationId? : Lean.Lsp.CreateFile → Option String
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Compatible.le_iff : ∀ {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β},
  H₁.Compatible H₂ → (H₁ ≤ H₂ ↔ H₁.vertexSet ⊆ H₂.vertexSet ∧ H₁.edgeSet ⊆ H₂.edgeSet)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.comp : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {u : Set M'},
  MDiffAt[u] g (f x) → MDiffAt[s] f x → s ⊆ f ⁻¹' u → MDiffAt[s] (g ∘ f) x
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.neg` -/
Meromorphic.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E}, Meromorphic f → Meromorphic fun i => -f i
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_concat : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (p₁.concat p₂) =
        Lean.Grind.CommRing.Poly.denoteS ctx p₁ + Lean.Grind.CommRing.Poly.denoteS ctx p₂
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_integral_density_of_antitone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ℕ → Set β),
      Antitone seq →
        ⋂ i, seq i = ∅ →
          (∀ (m : ℕ), MeasurableSet (seq m)) →
            Filter.Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃FunctorObj_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  {G₂₃ G₂₃' : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} (φ : G₂₃ ⟶ G₂₃') (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
  ((((CategoryTheory.bifunctorComp₂₃FunctorObj F).map φ).app X₁).app X₂).app X₃ = (F.obj X₁).map ((φ.app X₂).app X₃)
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instSetLike.eq_1 : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G],
  ClosedSubgroup.instSetLike G = { coe := fun U => ↑↑U, coe_injective := ⋯ }
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.mem_or_mem : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsPrime → ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult : Type
-- Lean.Expr
Lean.Expr.bvar.injEq : ∀ (deBruijnIndex deBruijnIndex_1 : ℕ),
  (Lean.Expr.bvar deBruijnIndex = Lean.Expr.bvar deBruijnIndex_1) = (deBruijnIndex = deBruijnIndex_1)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.tendsto_logb_nhdsGT_zero : ∀ {b : ℝ}, 1 < b → Filter.Tendsto (Real.logb b) (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot
-- Mathlib.RingTheory.Localization.Module
/-- A linear map `M →ₗ[R] N` gives a map between localized modules `Mₛ →ₗ[Rₛ] Nₛ`.  -/
LocalizedModule.map : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {N : Type u_3} →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] → (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
continuousAt_extChartAt_symm' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x x' : M},
  x' ∈ (extChartAt I x).source → ContinuousAt (↑(extChartAt I x).symm) (↑(extChartAt I x) x')
-- Mathlib.NumberTheory.WellApproximable
UnitAddCircle.mem_approxAddOrderOf_iff : ∀ {δ : ℝ} {x : UnitAddCircle} {n : ℕ},
  0 < n → (x ∈ approxAddOrderOf UnitAddCircle n δ ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ)
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- The forgetful functor from R-modules to abelian groups preserves all limits.
 -/
ModuleCat.forget₂AddCommGroup_preservesLimitsOfSize : ∀ {R : Type u} [inst : Ring R] [UnivLE.{v, w}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1}
    (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_counitIso_hom_app_toFun : ∀ (X : Bipointed) (a : ((Bipointed.swap.comp Bipointed.swap).obj X).X),
  (Bipointed.swapEquiv.counitIso.hom.app X).toFun a = a
-- Mathlib.RingTheory.Binomial
Ring.descPochhammer_succ_succ_smeval : ∀ {R : Type u_2} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (r : R) (k : ℕ),
  (descPochhammer ℤ (k + 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `lowerSemicontinuous_iff_le_liminf`. -/
LowerSemicontinuous.le_liminf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  LowerSemicontinuous f → ∀ (x : α), f x ≤ Filter.liminf f (nhds x)
-- Mathlib.Data.List.MinMax
List.maximum_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] (a : α), [a].maximum = ↑a
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.eq_2 : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u}
  {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} (it' : Std.IterM m β),
  Std.Iterators.Types.ULiftIterator.Monadic.modifyStep (Std.IterStep.skip it') =
    Std.IterStep.skip { internalState := { inner := it' } }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t₁ ∩ t₂).getKey? k = if k ∈ t₂ then t₁.getKey? k else none
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_injective_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S], Function.Surjective ⇑f → Function.Injective (Ideal.comap f)
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.CommRingCat.Hom.mk.injEq : ∀ {R S : CommRingCat} (hom' hom'_1 : ↑R →+* ↑S), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.FieldTheory.SeparableDegree
IntermediateField.finSepDegree_bot' : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Field.finSepDegree F ↥⊥ = Field.finSepDegree F E
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.neg_apply : ∀ {R : Type u_1} [inst : NegZeroClass R] {f : ArithmeticFunction R} {n : ℕ}, (-f) n = -f n
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.elabRunElab.unsafe_impl_4 : Lean.TSyntax `term → Lean.Elab.TermElabM (Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr)
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toAddSubmonoid_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p q : Submodule R M},
  p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.op_f₃₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.op.f₃₄ = sq.f₁₃.op
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.mk.congr_simp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (fst fst_1 : x.fst ⟶ y.fst) (e_fst : fst = fst_1) (snd snd_1 : x.snd ⟶ y.snd) (e_snd : snd = snd_1)
  (w :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst F) y.iso.hom =
      CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd G)),
  { fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := ⋯ }
-- Mathlib.Topology.CompactOpen
/-- **Alias** of `ContinuousMap.isOpen_setOfPred_range_subset`. -/
ContinuousMap.isOpen_setOf_range_subset : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {U : Set Y} [CompactSpace X],
  IsOpen U → IsOpen {f | Set.range ⇑f ⊆ U}
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmallerFnₘ.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match none with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {n : ℕ}
  (F : CategoryTheory.ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯)))
  (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows W F hF).isColimit.desc s =
    s.ι.app (Fin.last n)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- **Alias** of `perfectClosure.algEquivOfAlgEquiv`.

---

If `E` and `K` are isomorphic as `F`-algebras, then `perfectClosure F E` and
`perfectClosure F K` are also isomorphic as `F`-algebras.  -/
AlgEquiv.perfectClosure : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type w} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → ↥(perfectClosure F E) ≃ₐ[F] ↥(perfectClosure F K)
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_sup : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M N P : Submodule R A), M * (N ⊔ P) = M * N ⊔ M * P
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eval_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.eval 1 (Polynomial.Chebyshev.U R n) = ↑n + 1
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.cmp.match_1.eq_1 : ∀ (motive : ONote → ONote → Sort u_1) (h_1 : Unit → motive ONote.zero ONote.zero)
  (h_2 : (x : ONote) → motive x ONote.zero) (h_3 : (x : ONote) → motive ONote.zero x)
  (h_4 :
    (_o₁ e₁ : ONote) →
      (n₁ : ℕ+) →
        (a₁ : ONote) →
          _o₁ = e₁.oadd n₁ a₁ →
            (_o₂ e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → _o₂ = e₂.oadd n₂ a₂ → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)),
  (match ONote.zero, ONote.zero with
    | ONote.zero, ONote.zero => h_1 ()
    | x, ONote.zero => h_2 x
    | ONote.zero, x => h_3 x
    | _o₁@h:(e₁.oadd n₁ a₁), _o₂@h_5:(e₂.oadd n₂ a₂) => h_4 _o₁ e₁ n₁ a₁ h _o₂ e₂ n₂ a₂ h_5) =
    h_1 ()
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimitCocone_pt : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)),
  (AlgebraicGeometry.PresheafedSpace.colimitCocone F).pt = AlgebraicGeometry.PresheafedSpace.colimit F
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddHom.coe_ofDense : ∀ {M : Type u_1} {N : Type u_2} [inst : AddSemigroup M] [inst_1 : AddSemigroup N] {s : Set M} (f : M → N)
  (hs : AddSubsemigroup.closure s = ⊤) (hadd : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y),
  ⇑(AddHom.ofDense f hs hadd) = f
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.compMultilinearMapₗ.congr_simp : ∀ {R : Type uR} (S : Type uS) {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂]
  [inst_8 : AddCommMonoid M₃] [inst_9 : Module S M₃] [inst_10 : Module R M₃] [inst_11 : SMulCommClass R S M₃]
  [inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R] (g g_1 : M₂ →ₗ[R] M₃),
  g = g_1 → LinearMap.compMultilinearMapₗ S g = LinearMap.compMultilinearMapₗ S g_1
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι) (x : P.Ring),
  (Algebra.Generators.compLocalizationAwayAlgHom T g P)
      (((Algebra.Generators.localizationAway T g).toComp P).toAlgHom x) =
    (algebraMap P.Ring (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)))) x
-- Mathlib.Algebra.Ring.Defs
NonUnitalCommRing.mk : {α : Type u} → [toNonUnitalRing : NonUnitalRing α] → (∀ (a b : α), a * b = b * a) → NonUnitalCommRing α
-- Mathlib.Algebra.Expr
/-- Produce a `One` instance for `Q($α)` such that `1 : Q($α)` is `q(1 : $α)`.  -/
Expr.instOne : {u : Lean.Level} → (α : Q(Type u)) → Q(One «$α») → One Q(«$α»)
-- Mathlib.Algebra.Order.Group.PosPart
sup_eq_mul_oneLePart_div : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α] [MulLeftMono α] (a b : α), a ⊔ b = b * (a / b)⁺ᵐ
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegrable_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (a : E) (c : ℂ) (R : ℝ), CircleIntegrable (fun x => a) c R
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Icc_of_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ioc a b → x ∈ Set.Icc a b
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.iff_of_presieve : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocal K] {X : C} {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X → (P X ↔ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_eq : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) {a b c d : ℤ},
  d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2 →
    IsEllipticNet.atomRel W a b c d = IsEllipticNet.rel W ((a - d) / 2) ((b - d) / 2) ((c - d) / 2) d
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_mem_pow : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} {x : R}, x ∈ I → ∀ (n : ℕ), x ^ n ∈ I ^ n
-- Mathlib.Data.Finset.Preimage
Finset.image_preimage : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] (f : α → β) (s : Finset β)
  [inst_1 : (x : β) → Decidable (x ∈ Set.range f)] (hf : Set.InjOn f (f ⁻¹' ↑s)),
  Finset.image f (s.preimage f hf) = {x ∈ s | x ∈ Set.range f}
-- Init.Data.Dyadic.Basic
/-- Determine if a dyadic rational is strictly less than another.  -/
Dyadic.blt : Dyadic → Dyadic → Bool
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.constRingHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : NonAssocSemiring Y] (y : Y),
  LocallyConstant.constRingHom y = LocallyConstant.const X y
-- Mathlib.Algebra.Ring.Prod
/-- Product of two `NonUnitalCommSemiring`s is a `NonUnitalCommSemiring`.  -/
Prod.instNonUnitalCommSemiring : {R : Type u_1} → {S : Type u_3} → [NonUnitalCommSemiring R] → [NonUnitalCommSemiring S] → NonUnitalCommSemiring (R × S)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_update_sub : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι)
  (x y : M₁ i), f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Init.Data.Ord.Basic
compareOfLessAndEq.eq_1 : ∀ {α : Type u_1} (x y : α) [inst : LT α] [inst_1 : Decidable (x < y)] [inst_2 : DecidableEq α],
  compareOfLessAndEq x y = if x < y then Ordering.lt else if x = y then Ordering.eq else Ordering.gt
-- Mathlib.GroupTheory.GroupAction.SubMulAction
instMulActionElemFixedPointsSubtypeMemSubgroupOfNormal : {G : Type u_1} →
  [inst : Group G] →
    {α : Type u_2} →
      [inst_1 : MulAction G α] → {H : Subgroup G} → [hH : H.Normal] → MulAction G ↑(MulAction.fixedPoints (↥H) α)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors_val_eq_normalizedFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, IsRadical a → (UniqueFactorizationMonoid.primeFactors a).val = UniqueFactorizationMonoid.normalizedFactors a
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_ratCast_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : DivisionRing R] [inst_1 : AddCommGroup α]
  [inst_2 : StarAddMonoid α] [inst_3 : Module R α] (c : ℚ) (M : Matrix m n α),
  (↑c • M).conjTranspose = ↑c • M.conjTranspose
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (b : β k) (h_1 : Unit → motive none)
  (h_2 : (b : β k) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroup.seminormedAddCommGroup : {E : Type u_1} → [inst : SeminormedAddCommGroup E] → {s : AddSubgroup E} → SeminormedAddCommGroup ↥s
-- Mathlib.Order.SuccPred.Basic
PredOrder.ofOrderIso.eq_1 : ∀ {X : Type u_3} {Y : Type u_4} [inst : Preorder X] [inst_1 : Preorder Y] [inst_2 : PredOrder X] (f : X ≃o Y),
  PredOrder.ofOrderIso f =
    { pred := fun y => f (PredOrder.pred (f.symm y)), pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instBoundedContinuousMapClass : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β],
  BoundedContinuousMapClass (BoundedContinuousFunction α β) α β
-- Mathlib.Algebra.Quaternion
Quaternion.instNoZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R], NoZeroDivisors (Quaternion R)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The supremum of a chain in the product `ω`-CPO.  -/
Prod.ωSupImpl : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] → OmegaCompletePartialOrder.Chain (α × β) → α × β
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.proveEq?.tryAbstract : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  0 ≤ NumberField.mixedEmbedding.convexBodySumFun x
-- Mathlib.Data.Finsupp.ToDFinsupp
finsuppLequivDFinsupp_symm_apply : ∀ {ι : Type u_1} (R : Type u_2) {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)] [inst_4 : Module R M], ⇑(finsuppLequivDFinsupp R).symm = DFinsupp.toFinsupp
-- Mathlib.Tactic.ClickSuggestions.Util
/-- A global constant or a free variable. Library search can return either.  -/
Mathlib.Tactic.ClickSuggestions.Premise : Type
-- Mathlib.Order.FixedPoints
OrderHom.gfp_gfp : ∀ {α : Type u} [inst : CompleteLattice α] (h : α →o α →o α), OrderHom.gfp (OrderHom.gfp.comp h) = OrderHom.gfp h.onDiag