mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_maxKey!_eq_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : Std.Internal.List.containsKey (Std.Internal.List.maxKey! l) l = true},
      Std.Internal.List.getKey (Std.Internal.List.maxKey! l) l he = Std.Internal.List.maxKey l ⋯
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : ↥(MeasureTheory.Lp F p μ)},
  f ∈ MeasureTheory.lpMeasSubgroup F m p μ ↔ MeasureTheory.AEStronglyMeasurable (↑↑f) μ
-- Init.Data.Slice.Notation
/-- Slices `carrier` from `range.lower` \(exclusive\).
   -/
Std.Roi.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Roi.Sliceable α β γ] → α → Std.Roi β → γ
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R],
  ⌈1⌉₊ = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {fallback : β}, Std.DTreeMap.Raw.Const.getD (t.erase k) k fallback = fallback
-- Lean.Parser.Term
Lean.Parser.Term.dotIdent.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.ofPresheaf_obj_carrier : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : CategoryTheory.Functor Cᵒᵖ Ab) [inst_1 : (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)]
  (map_smul :
    ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)),
      (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
        (CategoryTheory.ConcreteCategory.hom (R.map f)) r • (CategoryTheory.ConcreteCategory.hom (M.map f)) m)
  (X : Cᵒᵖ), ↑((PresheafOfModules.ofPresheaf M map_smul).obj X) = ↑(M.obj X)
-- Mathlib.Analysis.Calculus.Taylor
/-- Calculate the derivative of the Taylor polynomial with respect to `x₀`.

Version for closed intervals  -/
hasDerivWithinAt_taylorWithinEval_at_Icc : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ},
  a < b →
    t ∈ Set.Icc a b →
      ContDiffOn ℝ (↑n) f (Set.Icc a b) →
        DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc a b)) (Set.Icc a b) →
          HasDerivWithinAt (fun y => taylorWithinEval f n (Set.Icc a b) y x)
            (((↑n.factorial)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Set.Icc a b) t) (Set.Icc a b) t
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_eq_none : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∉ m → m[a]? = none
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `h ≫ f⟦1⟧ = 0`.  -/
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.CategoryStruct.comp T.mor₃ ((CategoryTheory.shiftFunctor C 1).map T.mor₁) = 0
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.smul_apply : ∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens} (r : ↑(X.presheaf.obj (Opposite.op U)))
  (x : ↑(M.presheaf.obj (Opposite.op U))), (AddCommGrpCat.Hom.hom (AlgebraicGeometry.Scheme.Modules.smul r)) x = r • x
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_of_arrow_mk_iso : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L K' L' : HomologicalComplex C c}
  (φ : K ⟶ L) (φ' : K' ⟶ L') (e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ')
  [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i] [inst_4 : ∀ (i : ι), K'.HasHomology i]
  [inst_5 : ∀ (i : ι), L'.HasHomology i] [hφ : QuasiIso φ], QuasiIso φ'
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.VAddInvariantMeasure.vadd_nnreal : ∀ {M : Type v} {α : Type w} [inst : VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.VAddInvariantMeasure M α μ] (c : NNReal), MeasureTheory.VAddInvariantMeasure M α (c • μ)
-- Init.Data.Int.Order
Int.lt_or_lt_of_ne : ∀ {a b : ℤ}, a ≠ b → a < b ∨ b < a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofDistribMulAction_ρ_apply_apply : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] (A : Type w') [inst_2 : AddCommGroup A]
  [inst_3 : Module k A] [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] (g : G) (a : A),
  ((Rep.ofDistribMulAction k G A).ρ g) a = g • a
-- Mathlib.Computability.Encoding
/-- Deprecated alias for `encodingList`.  -/
Computability.finEncodingList : (α : Type) → [Fintype α] → Computability.Encoding (List α) α
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_mem_one : ∀ {α : Type u_2} [inst : One α], 1 ∈ 1
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instSub : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → Sub (M →ₗ⁅R,L⁆ N)
-- Mathlib.Analysis.MellinTransform
/-- A function `f` is `VerticalIntegrable` at `σ` if `y ↦ f(σ + yi)` is integrable.  -/
Complex.VerticalIntegrable : {E : Type u_1} →
  [NormedAddCommGroup E] → (ℂ → E) → ℝ → autoParam (MeasureTheory.Measure ℝ) Complex.VerticalIntegrable._auto_1 → Prop
-- Mathlib.Order.UpperLower.CompleteLattice
/-- An order isomorphism of Preorders induces an order isomorphism of their upper sets.  -/
UpperSet.map : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → UpperSet α ≃o UpperSet β
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- A `LocallyRingedSpace` is a topological space equipped with a sheaf of commutative rings
such that all the stalks are local rings.

A morphism of locally ringed spaces is a morphism of ringed spaces
such that the morphisms induced on stalks are local ring homomorphisms.  -/
AlgebraicGeometry.LocallyRingedSpace : Type (u + 1)
-- Init.Data.UInt.Bitwise
UInt16.xor_self : ∀ {a : UInt16}, a ^^^ a = 0
-- Mathlib.Data.Nat.Prime.Defs
Nat.le_minFac' : ∀ {m n : ℕ}, n = 1 ∨ m ≤ n.minFac ↔ ∀ (p : ℕ), 2 ≤ p → p ∣ n → m ≤ p
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.intCoe_mul : ∀ {R : Type u_1} [inst : Ring R] {f g : ArithmeticFunction ℤ}, ↑(f * g) = ↑f * ↑g
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
IsDiscreteValuationRing.associated_of_valuation_eq : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDiscreteValuationRing A]
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x y : K),
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal A)) x =
      (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal A)) y →
    ∃ u, u • x = y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → ∀ {fallback : α}, t.maxKeyD fallback = fallback
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle.inj : ∀ {lhs : Bool} {s₁ s₂ : Lean.Grind.AC.Seq} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {c₂ : Lean.Meta.Grind.AC.DiseqCnstr}
  {lhs_1 : Bool} {s₁_1 s₂_1 : Lean.Grind.AC.Seq} {c₁_1 : Lean.Meta.Grind.AC.EqCnstr}
  {c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle lhs s₁ s₂ c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle lhs_1 s₁_1 s₂_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s₁ = s₁_1 ∧ s₂ = s₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Algebra.CharP.Algebra
Algebra.charP_iff : ∀ (K : Type u_3) (L : Type u_4) [inst : Field K] [inst_1 : CommSemiring L] [Nontrivial L] [Algebra K L] (p : ℕ),
  CharP K p ↔ CharP L p
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.buildReify.mkPS : Lean.Expr → ℕ → Lean.Expr → ℕ → Lean.Expr
-- Mathlib.Order.Zorn
zorn_le_nonempty₀ : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α),
  (∀ c ⊆ s, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) →
    ∀ x ∈ s, ∃ m, x ≤ m ∧ Maximal (fun x => x ∈ s) m
-- Mathlib.RingTheory.Spectrum.Maximal.Topology
/-- The Zariski topology on the maximal spectrum of a commutative ring is defined as the subspace
topology induced by the natural inclusion into the prime spectrum.  -/
MaximalSpectrum.zariskiTopology : {R : Type u} → [inst : CommRing R] → TopologicalSpace (MaximalSpectrum R)
-- Std.Data.TreeMap.Basic
/-- Creates a new empty tree map. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree map. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeMap.empty : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isPreconnected_closedBall : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ}, IsPreconnected (Metric.closedBall x r)
-- Mathlib.Algebra.Group.Action.Sum
Sum.smul_swap : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] (a : M) (x : α ⊕ β),
  (a • x).swap = a • x.swap
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (D : ℝ) (x : E), 0 ≤ ExistsContDiffBumpBase.y D x
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.hom_comp : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T),
  CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)
-- Mathlib.Order.Interval.Set.Defs
Set.Iic_def : ∀ {α : Type u_1} [inst : Preorder α] (b : α), {x | x ≤ b} = Set.Iic b
-- Mathlib.CategoryTheory.Functor.Const
/-- The constant functor `Jᵒᵖ ⥤ C` sending everything to `unop X`
is (naturally isomorphic to) the opposite of
the constant functor `J ⥤ Cᵒᵖ` sending everything to `X`.
 -/
CategoryTheory.Functor.const.opObjUnop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        (X : Cᵒᵖ) →
          (CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.unop X) ≅ ((CategoryTheory.Functor.const J).obj X).leftOp
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nfBelow_ofNat : ∀ (n : ℕ), (↑n).NFBelow 1
-- Mathlib.ModelTheory.Syntax
/-- Applies a binary function to two terms.  -/
FirstOrder.Language.Functions.apply₂ : {L : FirstOrder.Language} → {α : Type u'} → L.Functions 2 → L.Term α → L.Term α → L.Term α
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.domRestrict_eq_one_iff : ∀ {M : Type u_1} [inst : MulOneClass M] {N : Type u_5} {S : Type u_6} [inst_1 : MulOneClass N] {f : M →* N}
  [inst_2 : SetLike S M] [inst_3 : SubmonoidClass S M] {s : S}, f.domRestrict s = 1 ↔ ∀ x ∈ s, f x = 1
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.zero : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂], LinearMap.HasNoetherianRange 0
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_enum : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {o : Ordinal.{u}} (h : o < Ordinal.type r),
  (Ordinal.typein r).toRelEmbedding ((Ordinal.enum r) ⟨o, h⟩) = o
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mk.inj : ∀ {R : Type u} {inst : NonAssocRing R} {toSubsemiring : Subsemiring R}
  {neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier} {toSubsemiring_1 : Subsemiring R}
  {neg_mem'_1 : ∀ {x : R}, x ∈ toSubsemiring_1.carrier → -x ∈ toSubsemiring_1.carrier},
  { toSubsemiring := toSubsemiring, neg_mem' := neg_mem' } =
      { toSubsemiring := toSubsemiring_1, neg_mem' := neg_mem'_1 } →
    toSubsemiring = toSubsemiring_1
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.IsRestricted.eq_1 : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) (f : PowerSeries R),
  PowerSeries.IsRestricted c f = MvPowerSeries.IsRestricted (fun x => c) f
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.toStarRing : {A : Type u_1} → [self : CommCStarAlgebra A] → StarRing A
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Poly.denoteN.match_1.eq_1 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (match Lean.Grind.Linarith.Poly.nil with
    | Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add k v p => h_2 k v p) =
    h_1 ()
-- Mathlib.Analysis.LocallyConvex.Bounded
NormedSpace.isVonNBounded_iff' : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r
-- Mathlib.RingTheory.ZMod.Torsion
ZMod.instHasEnoughRootsOfUnityHSubNatOfNat : ∀ {p : ℕ} [Fact (Nat.Prime p)], HasEnoughRootsOfUnity (ZMod p) (p - 1)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Typecheck a `MonoidHom` as a morphism in `GrpCat`.  -/
GrpCat.ofHom : {X Y : Type u} → [inst : Group X] → [inst_1 : Group Y] → (X →* Y) → (GrpCat.of X ⟶ GrpCat.of Y)
-- Mathlib.Algebra.Order.Group.Synonym
isAddRegular_toLex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddRegular (toLex a) ↔ IsAddRegular a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_add_nat_mul_pi : ∀ (x : ℂ) (n : ℕ), Complex.tan (x + ↑n * ↑Real.pi) = Complex.tan x
-- Init.Data.SInt.Basic
Int16.ofUInt16.injEq : ∀ (toUInt16 toUInt16_1 : UInt16), ({ toUInt16 := toUInt16 } = { toUInt16 := toUInt16_1 }) = (toUInt16 = toUInt16_1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Mathlib.Data.WSeq.Basic
/-- Destruct a weak sequence, to (eventually possibly) produce either
`none` for `nil` or `some (a, s)` if an element is produced.  -/
Stream'.WSeq.destruct : {α : Type u} → Stream'.WSeq α → Computation (Option (α × Stream'.WSeq α))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.map₂ α β).obj X).hom =
    CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (G.map X.hom) β)
-- Mathlib.Topology.Algebra.Algebra
/-- `Prod.map` of two continuous algebra homomorphisms.  -/
ContinuousAlgHom.prodMap : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] →
                  [inst_6 : Algebra R B] →
                    {C : Type u_4} →
                      [inst_7 : Semiring C] →
                        [inst_8 : Algebra R C] →
                          [inst_9 : TopologicalSpace C] →
                            {D : Type u_5} →
                              [inst_10 : Semiring D] →
                                [inst_11 : TopologicalSpace D] →
                                  [inst_12 : Algebra R D] → (A →A[R] B) → (C →A[R] D) → A × C →A[R] B × D
-- Mathlib.Data.Quot
Quotient.eq' : ∀ {α : Sort u_1} {s₁ : Setoid α} {a b : α}, Quotient.mk' a = Quotient.mk' b ↔ s₁ a b
-- Mathlib.Control.Applicative
Functor.Comp.instCommApplicative : ∀ {f : Type u → Type w} {g : Type v → Type u} [inst : Applicative f] [inst_1 : Applicative g] [CommApplicative f]
  [CommApplicative g], CommApplicative (Functor.Comp f g)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.center_ne_iff_ne_of_mem : ∀ {P : Type u_2} [inst : MetricSpace P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  p ∈ s₁ → p ∈ s₂ → (s₁.center ≠ s₂.center ↔ s₁ ≠ s₂)
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_zero : ∀ {w i : ℕ}, (0#w).getLsbD i = false
-- Init.Data.List.Scan.Lemmas
List.getElem_scanl : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {a : α} {l : List β} {f : α → β → α} (h : i < (List.scanl f a l).length),
  (List.scanl f a l)[i] = List.foldl f a (List.take i l)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_mul_X : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
  Polynomial.eval₂ f x (p * Polynomial.X) = Polynomial.eval₂ f x p * x
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.le_centralizer : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [h : IsAddCommutative ↥H], H ≤ AddSubgroup.centralizer ↑H
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.compare_getKey_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  (h' : k ∈ t), cmp (t.getKey k h') k = Ordering.eq
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.linearHom_apply : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (self : P1 →ᵃ[k] P1), AffineMap.linearHom self = self.linear
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instAddZeroClass.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddZeroClass R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R],
  BoundedContinuousFunction.instAddZeroClass =
    { toZero := BoundedContinuousFunction.instZero, toAdd := BoundedContinuousFunction.instAdd, zero_add := ⋯,
      add_zero := ⋯ }
-- Mathlib.Algebra.Star.Module
IsIdempotentElem.star_iff : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {a : R}, IsIdempotentElem (star a) ↔ IsIdempotentElem a
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.mul : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop} (j : J)
  (x y : ↑(F.obj j)), MonCat.Colimits.Relation.below ⋯
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.homeomorphOfUnique_apply : ∀ (X : Type u_1) (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Unique X]
  [inst_3 : Unique Y] (a : X), (Homeomorph.homeomorphOfUnique X Y) a = default
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.mk.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (asIdeal asIdeal_1 : Ideal R) (e_asIdeal : asIdeal = asIdeal_1)
  (isPrime : asIdeal.IsPrime), { asIdeal := asIdeal, isPrime := isPrime } = { asIdeal := asIdeal_1, isPrime := ⋯ }
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- A bialgebra homomorphism `R[G] → R[H]` between group algebras over a domain `R` comes from a
group hom `G → H`.

See `MonoidAlgebra.mapDomainBialgHom` for the forward map.  -/
AddMonoidAlgebra.mapDomainOfBialgHom : {R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] →
          [inst_2 : AddGroup G] → [inst_3 : AddGroup H] → (AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) → G →+ H
-- Lean.Data.KVMap
Lean.KVMap.Value.toDataValue : {α : Type} → [self : Lean.KVMap.Value α] → α → Lean.DataValue
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] (f : β → α) {b : β}, {b}.inf' ⋯ f = f b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.ExtHashMap.unitOfList l).getKey? k = none
-- Mathlib.Order.Filter.Map
Filter.comap_inl_map_inr : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β}, Filter.comap Sum.inl (Filter.map Sum.inr g) = ⊥
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- If `𝕜` is a topological module over a semiring `R` and scalar multiplication commutes with the
multiplication on `𝕜`, then `WeakDual 𝕜 E` is a module over `R`.  -/
WeakDual.instModule' : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] →
                [inst_6 : TopologicalSpace E] →
                  (R : Type u_6) →
                    [inst_7 : Semiring R] →
                      [inst_8 : Module R 𝕜] →
                        [SMulCommClass 𝕜 R 𝕜] → [ContinuousConstSMul R 𝕜] → Module R (WeakDual 𝕜 E)
-- Mathlib.CategoryTheory.Galois.EssSurj
/-- If `X` is connected and `x` is in the fiber of `X`, `F.obj X` is isomorphic
to the quotient of `Aut F` by the stabilizer of `x` as `Aut F`-sets.  -/
CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizer : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (X : C) →
            [CategoryTheory.PreGaloisCategory.IsConnected X] →
              (x : (F.obj X).obj) →
                (CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅
                  Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
                    (FintypeCat.of (CategoryTheory.Aut F ⧸ MulAction.stabilizer (CategoryTheory.Aut F) x))
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.restrict_ofFunction : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α),
  Monotone m →
    (MeasureTheory.OuterMeasure.restrict s) (MeasureTheory.OuterMeasure.ofFunction m m_empty) =
      MeasureTheory.OuterMeasure.ofFunction (fun t => m (t ∩ s)) ⋯
-- Init.Data.Option.Lemmas
Option.or_eq_left_of_isSome : ∀ {α : Type u_1} {o o' : Option α}, o.isSome = true → o.or o' = o
-- Lean.LocalContext
_private.Lean.LocalContext.0.Lean.LocalContext.mkLetDeclExported : Lean.LocalContext → Lean.FVarId → Lean.Name → Lean.Expr → Lean.Expr → Bool → Lean.LocalContext
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
Submonoid.le_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : GroupWithZero G₀] [inst_2 : MulDistribMulAction G₀ M]
  {a : G₀}, a ≠ 0 → ∀ {S T : Submonoid M}, S ≤ a • T ↔ a⁻¹ • S ≤ T