mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_sub : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c c' : ℕ → 𝕜),
  FormalMultilinearSeries.ofScalars E (c - c') =
    FormalMultilinearSeries.ofScalars E c - FormalMultilinearSeries.ofScalars E c'
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.IsLocalizedModule.localized'FrameHom_apply : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (M' : Submodule R M),
  (Submodule.localized'FrameHom S p f) M' = Submodule.localized' S p f M'
-- Init.Data.BitVec.Lemmas
/-- The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
 -/
BitVec.toInt_intMin : ∀ {w : ℕ}, (BitVec.intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)
-- Init.Data.Int.Gcd
Int.gcd_eq_natAbs_left_iff_dvd : ∀ {a b : ℤ}, a.gcd b = a.natAbs ↔ a ∣ b
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.comap_boundedBy : ∀ {α : Type u_1} {m : Set α → ENNReal} {β : Type u_2} (f : β → α),
  (Monotone fun s => m ↑s) ∨ Function.Surjective f →
    (MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.boundedBy m) =
      MeasureTheory.OuterMeasure.boundedBy fun s => m (f '' s)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instOfSomeENatTopOfLEInfty : ∀ {𝕜 : 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] {a : WithTop ℕ∞} [IsManifold I (↑⊤) M] [h : ENat.LEInfty a],
  IsManifold I a M
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- If `x` is a transcendence basis of `A/R`, then it is not empty if and only if
`A/R` is transcendental.  -/
IsTranscendenceBasis.nonempty_iff_transcendental : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R], IsTranscendenceBasis R x → (Nonempty ι ↔ Algebra.Transcendental R A)
-- Mathlib.Data.Matrix.Reflection
/-- Expand `A` to `!![A 0 0, ...; ..., A m n]`  -/
Matrix.etaExpand : {α : Type u_1} → {m n : ℕ} → Matrix (Fin m) (Fin n) α → Matrix (Fin m) (Fin n) α
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.finite_subcomplex_top_iff : ∀ (X : SSet), ⊤.toSSet.Finite ↔ X.Finite
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_insertNth_add : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂) (p : Fin (n + 1))
  (m : (i : Fin n) → M (p.succAbove i)) (x y : M p),
  f (p.insertNth (x + y) m) = f (p.insertNth x m) + f (p.insertNth y m)
-- Mathlib.Topology.Algebra.Order.Field
Filter.Tendsto.inv_tendsto_nhdsGT_zero : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f : α → 𝕜},
  Filter.Tendsto f l (nhdsWithin 0 (Set.Ioi 0)) → Filter.Tendsto f⁻¹ l Filter.atTop
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.left_unitor_hom_inv : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b), CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_toSubsemiring : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R Aᵐᵒᵖ), S.unop.toSubsemiring = S.unop
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.mul_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a b : α) (v₁ v₂ v : ℚ),
  (v == v₁ * v₂) = true →
    a = Lean.Grind.Field.NormNum.ofRat v₁ →
      b = Lean.Grind.Field.NormNum.ofRat v₂ → a * b = Lean.Grind.Field.NormNum.ofRat v
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.deriv_smul : ∀ {g : GL (Fin 2) ℝ},
  0 < (↑g).det →
    ∀ (τ : UpperHalfPlane),
      deriv (fun z => ↑(g • ↑UpperHalfPlane.ofComplex z)) ↑τ = ↑(↑g).det / UpperHalfPlane.denom g ↑τ ^ 2
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.support_eq_empty : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {p : SkewMonoidAlgebra k G}, p.support = ∅ ↔ p = 0
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
Cardinal.not_injective_limitation_set : ∀ {α : Type u} (g : Ordinal.{u} → α), ¬Set.InjOn g (Set.Iio (SuccOrder.succ (Cardinal.mk α)).ord)
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- The extension of a map `f : α → M` that satisfies the given relations to an
additive-monoid homomorphism from `PresentedAddMonoid rels → M`  -/
PresentedAddMonoid.lift : {α : Type u_3} →
  {M : Type u_4} →
    [inst : AddMonoid M] →
      (f : α → M) →
        {rels : FreeAddMonoid α → FreeAddMonoid α → Prop} →
          (∀ (a b : FreeAddMonoid α), rels a b → (FreeAddMonoid.lift f) a = (FreeAddMonoid.lift f) b) →
            PresentedAddMonoid rels →+ M
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- Equality of maps out of an adic completion can be checked on Cauchy sequences.  -/
AdicCompletion.map_ext : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Sort u_6} {f g : AdicCompletion I M → N},
  (∀ (a : AdicCompletion.AdicCauchySequence I M), f ((AdicCompletion.mk I M) a) = g ((AdicCompletion.mk I M) a)) → f = g
-- Init.Data.List.Lemmas
List.map_inj_right : ∀ {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → β},
  (∀ (x y : α), f x = f y → x = y) → (List.map f l = List.map f l' ↔ l = l')
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [NoMinOrder α], (Set.Iio a).Nonempty
-- Mathlib.FieldTheory.Differential.Liouville
/-- If `K` is a Liouville extension of `F` and `B` is a finite-dimensional intermediate
field `K / B / F`, then it's also a Liouville extension of `F`.
 -/
instIsLiouvilleSubtypeMemIntermediateField : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K] [DifferentialAlgebra F K] [inst_6 : CharZero F] (B : IntermediateField F K)
  [inst_7 : FiniteDimensional F ↥B] [inst_8 : IsLiouville F K], IsLiouville F ↥B
-- Mathlib.Data.List.Permutation
List.map_permutationsAux : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (ts is : List α),
  List.map (List.map f) (ts.permutationsAux is) = (List.map f ts).permutationsAux (List.map f is)
-- Mathlib.Order.Monotone.Monovary
/-- `f` antivaries with `g` if `g i < g j` implies `f j ≤ f i`.  -/
Antivary : {ι : Type u_1} → {α : Type u_3} → {β : Type u_4} → [Preorder α] → [Preorder β] → (ι → α) → (ι → β) → Prop
-- Init.Data.String.Decode
UInt8.utf8ByteSize.eq_1 : ∀ (c : UInt8) (_h : c.IsUTF8FirstByte),
  c.utf8ByteSize _h = if c &&& 128 = 0 then 1 else if c &&& 224 = 192 then 2 else if c &&& 240 = 224 then 3 else 4
-- Mathlib.Tactic.Sat.FromLRAT
/-- Formula `f` subsumes `f'` if all the clauses in `f'` are in `f`.
We use this to prove that all clauses in the formula are subsumed by it.  -/
Sat.Fmla.subsumes : Sat.Fmla → Sat.Fmla → Prop
-- Std.Data.TreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the largest key.
 -/
Std.TreeMap.maxKey : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → (t : Std.TreeMap α β cmp) → t.isEmpty = false → α
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.incl_coe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  ↑I.incl = (LieIdeal.toLieSubalgebra R L I).subtype
-- Mathlib.LinearAlgebra.Dimension.Torsion.Finite
Module.IsTorsion.finrank_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R],
  Module.IsTorsion R M → Module.finrank R M = 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.updateCell.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (hl : l.Balanced) →
          ((hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl) →
            ((sz : ℕ) →
                (ky : α) →
                  (y : β ky) →
                    (l r : Std.DTreeMap.Internal.Impl α β) →
                      (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) →
                        motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl) →
              motive l hl
-- Mathlib.Algebra.Lie.Derivation.Killing
LieDerivation.IsKilling.ad_apply_eq_zero_iff : ∀ (R : Type u_1) (L : Type u_2) [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Module.Finite R L]
  [LieAlgebra.IsKilling R L] (x : L), (LieDerivation.ad R L) x = 0 ↔ x = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- The `Mulstruct` for a simplicial set `X` that is deduced from a `Mulstruct` for `X.op`.  -/
SSet.PtSimplex.MulStruct.unop : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g fg : X.PtSimplex n x} →
        {i : Fin n} →
          g.op.MulStruct f.op fg.op i →
            {j : Fin n} → autoParam (i.rev = j) SSet.PtSimplex.MulStruct.unop._auto_1 → f.MulStruct g fg j
-- Lean.Expr
/-- Return `true` if the given expression is a non-dependent let-expression (a have-expression).  -/
Lean.Expr.isHave : Lean.Expr → Bool
-- Mathlib.Data.Finmap
/-- Fold a commutative function over the key-value pairs in the map  -/
Finmap.foldl : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      (f : δ → (a : α) → β a → δ) →
        (∀ (d : δ) (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂), f (f d a₁ b₁) a₂ b₂ = f (f d a₂ b₂) a₁ b₁) →
          δ → Finmap β → δ
-- Init.Data.List.Nat.BEq
List.beq_eq_isEqv : ∀ {α : Type u_1} [inst : BEq α] {as bs : List α}, as.beq bs = as.isEqv bs fun x1 x2 => x1 == x2
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms], P.op.IsClosedUnderIsomorphisms
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.PseudoCore.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.LaxFunctor B C} →
          (mapIdIso :
              (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)) →
            (mapCompIso :
                {a b c : B} →
                  (f : a ⟶ b) →
                    (g : b ⟶ c) →
                      F.map (CategoryTheory.CategoryStruct.comp f g) ≅
                        CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) →
              autoParam (∀ {a : B}, (mapIdIso a).inv = F.mapId a)
                  CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv._autoParam →
                autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).inv = F.mapComp f g)
                    CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv._autoParam →
                  F.PseudoCore
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.edist_integral_le_lintegral_edist : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f g : α → G},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → edist (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ≤ ∫⁻ (a : α), edist (f a) (g a) ∂μ
-- Lean.DefEqAttrib
_private.Lean.DefEqAttrib.0.Lean.isRflProofCore : Lean.Expr → Lean.Expr → Lean.CoreM Bool
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_intCast : ∀ {R : Type u_3} [inst : CommRing R] (z : ℤ), Quaternion.normSq ↑z = ↑z ^ 2
-- Lean.DeclarationRange
Lean.findDeclarationRangesCore? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Lean.DeclarationRanges)
-- Lean.Server.Requests
Lean.Server.RequestHandlerCompleteness.partial.injEq : ∀ (refreshMethod : String) (refreshIntervalMs : ℕ) (refreshMethod_1 : String) (refreshIntervalMs_1 : ℕ),
  (Lean.Server.RequestHandlerCompleteness.partial refreshMethod refreshIntervalMs =
      Lean.Server.RequestHandlerCompleteness.partial refreshMethod_1 refreshIntervalMs_1) =
    (refreshMethod = refreshMethod_1 ∧ refreshIntervalMs = refreshIntervalMs_1)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opcyclesOpIso_hom_naturality_assoc : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] {Z : Vᵒᵖ} (h : Opposite.op (K.cycles i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((HomologicalComplex.opFunctor V c).map φ.op) i)
      (CategoryTheory.CategoryStruct.comp (K.opcyclesOpIso i).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (L.opcyclesOpIso i).hom (HomologicalComplex.cyclesMap φ i).op) h
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cochainsIso₀.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.cochainsIso₀ A = (LinearEquiv.funUnique (Fin 0 → G) k ↑A).toModuleIso
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.Pos.skipWhile.match_1.splitter : {s : String.Slice} →
  (motive : Option s.Pos → Sort u_1) →
    (x : Option s.Pos) → ((nextCurr : s.Pos) → motive (some nextCurr)) → (Unit → motive none) → motive x
-- Mathlib.Data.QPF.Univariate.Basic
/-- The maximal congruence on `q.P.M`.  -/
QPF.Mcongr : {F : Type u → Type u} → [q : QPF F] → (QPF.P F).M → (QPF.P F).M → Prop
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.coe_singletonSubgraph : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V), (G.singletonSubgraph v).coe.IsTree
-- Mathlib.Logic.Relation
Relation.reflTransGen_iff_eq_or_transGen : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Relation.ReflTransGen r a b ↔ b = a ∨ Relation.TransGen r a b
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.toAdditive_symm_apply_symm_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : MulOneClass H] (f : Additive G ≃+ Additive H) (a : H),
  (MulEquiv.toAdditive.symm f).symm a = (MonoidHom.toAdditive.symm f.symm.toAddMonoidHom) a
-- Mathlib.GroupTheory.OrderOfElement
finite_powers : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] {a : G}, (↑(Submonoid.powers a)).Finite ↔ IsOfFinOrder a
-- Init.Control.Lawful.Basic
Id.run_seqRight : ∀ {α β : Type u_1} (x : Id α) (y : Id β), (x *> y).run = y.run
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommMon C),
  (CategoryTheory.Functor.mapCommMonIdIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).getD k' fallback = cast ⋯ v
-- Mathlib.Analysis.MeanInequalities
Real.Lp_add_le_tsum_of_nonneg' : ∀ {ι : Type u} {f g : ι → ℝ} {p : ℝ},
  1 ≤ p →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) →
          (Summable fun i => g i ^ p) →
            (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
-- Init.Data.Char.Lemmas
Char.val_inj : ∀ {c d : Char}, c.val = d.val ↔ c = d
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- A generalization of `galRestrictHom` beyond endomorphisms.  -/
galRestrict' : (A : Type u_1) →
  {K : Type u_2} →
    {L : Type u_3} →
      {L₂ : Type u_4} →
        (B : Type u_6) →
          (B₂ : Type u_7) →
            [inst : CommRing A] →
              [inst_1 : CommRing B] →
                [inst_2 : CommRing B₂] →
                  [inst_3 : Algebra A B] →
                    [inst_4 : Algebra A B₂] →
                      [inst_5 : Field K] →
                        [inst_6 : Field L] →
                          [inst_7 : Field L₂] →
                            [inst_8 : Algebra A K] →
                              [inst_9 : Algebra K L] →
                                [inst_10 : Algebra A L] →
                                  [IsScalarTower A K L] →
                                    [inst_12 : Algebra K L₂] →
                                      [inst_13 : Algebra A L₂] →
                                        [IsScalarTower A K L₂] →
                                          [inst_15 : Algebra B L] →
                                            [IsScalarTower A B L] →
                                              [IsIntegralClosure B A L] →
                                                [inst_18 : Algebra B₂ L₂] →
                                                  [IsScalarTower A B₂ L₂] →
                                                    [IsIntegralClosure B₂ A L₂] → (L →ₐ[K] L₂) → B →ₐ[A] B₂
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.hasSum_integral_iUnion_ae : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [Countable ι] {s : ι → Set X},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
      MeasureTheory.IntegrableOn f (⋃ i, s i) μ →
        HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ n, s n, f x ∂μ)
-- Mathlib.Topology.NhdsKer
nhdsKer_union : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s t : Set X), nhdsKer (s ∪ t) = nhdsKer s ∪ nhdsKer t
-- Mathlib.Algebra.GroupWithZero.Basic
/-- To match `mul_one_eq_id`.  -/
mul_zero_eq_const : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀], (fun x => x * 0) = Function.const M₀ 0
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.trans : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} ⦃p₀ p₁ p₂ : Path x₀ x₁⦄,
  p₀.Homotopic p₁ → p₁.Homotopic p₂ → p₀.Homotopic p₂
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesFiniteColimits.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam
      (∀ (J : Type) [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
        CategoryTheory.Limits.PreservesColimitsOfShape J F)
      CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits._autoParam →
    CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.CategoryTheory.Category.PartialFun
/-- The functor which deletes the point of a pointed type. In return, this makes the maps partial.
This is the computable part of the equivalence `PartialFunEquivPointed`.  -/
pointedToPartialFun : CategoryTheory.Functor Pointed PartialFun
-- Init.Data.List.Perm
List.perm_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, l.Perm (List.replicate n a) ↔ l = List.replicate n a
-- Mathlib.Topology.Algebra.ConstMulAction
vadd_mem_nhds_vadd_iff : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] {t : Set α} (g : G) {a : α}, g +ᵥ t ∈ nhds (g +ᵥ a) ↔ t ∈ nhds a
-- Mathlib.Geometry.Manifold.DerivationBundle
PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf : ∀ {𝕜 : 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] {x : M},
  IsScalarTower 𝕜 (PointedContMDiffMap 𝕜 I M (↑⊤) x) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- If the `p`-adic norm of `q` is 0, then `q` is `0`.  -/
padicNorm.zero_of_padicNorm_eq_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ}, padicNorm p q = 0 → q = 0
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjoint.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (T : E →ₗ.[𝕜] F)
  [inst_5 : CompleteSpace E],
  T.adjoint = { domain := T.adjointDomain, toFun := if hT : Dense ↑T.domain then LinearPMap.adjointAux hT else 0 }
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationParams : Type
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.coalgebraEquivOver.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  CategoryTheory.coalgebraEquivOver X =
    { functor := CategoryTheory.coalgebraToOver X, inverse := CategoryTheory.overToCoalgebra X,
      unitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun A =>
            CategoryTheory.Comonad.Coalgebra.isoMk
              (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.prodComonad X).Coalgebra).obj A).A)
              ⋯)
          ⋯,
      counitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun f =>
            CategoryTheory.Over.isoMk
              (CategoryTheory.Iso.refl
                (((CategoryTheory.overToCoalgebra X).comp (CategoryTheory.coalgebraToOver X)).obj f).left)
              ⋯)
          ⋯,
      functor_unitIso_comp := ⋯ }
-- Lean.Widget.InteractiveGoal
/-- The value, in the case the hypothesis is a `let`-binder.  -/
Lean.Widget.InteractiveHypothesisBundle.val? : Lean.Widget.InteractiveHypothesisBundle → Option Lean.Widget.CodeWithInfos
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The identity relating the isomorphisms between `X ⊗ (𝟙_ C ⊗ Y)`, `(X ⊗ 𝟙_ C) ⊗ Y` and `X ⊗ Y`
 -/
CategoryTheory.MonoidalCategory.triangle : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y