mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.mem_fixingSubgroup_iff : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (α : Gal(K/k))
  (L : FiniteGaloisIntermediateField k K),
  α ∈ L.fixingSubgroup ↔ (AlgEquiv.restrictNormalHom ↥L.toIntermediateField) α = 1
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_univ_left : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] [inst_2 : Fintype α] (t : Finset α),
  Finset.univ.mulEnergy t = Fintype.card α * t.card ^ 2
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Icc_iff_integrableOn_Ioo : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α} [MeasureTheory.NullSingletonClass μ],
  autoParam (‖f a‖ₑ ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ioo._auto_1 →
    autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ioo._auto_3 →
      (MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₂ = f.f₀.τ₃
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- A `PartialEquiv` which is continuous on its source and has open forward map (on its source) and
open source is a `PartialHomeomorph`.  -/
PartialHomeomorph.ofContinuousOpen : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : PartialEquiv X Y) → ContinuousOn (↑e) e.source → IsOpenMap ↑e → IsOpen e.source → PartialHomeomorph X Y
-- Init.Data.Fin.Fold
Fin.foldr.loop.eq_1 : ∀ {α : Sort u_1} (n : ℕ) (f : Fin n → α → α) (a : α) (x_3 : 0 ≤ n), Fin.foldr.loop n f 0 x_3 a = a
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffWithinAt.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E},
  UniqueDiffWithinAt 𝕜 s x → t ∈ nhds x → UniqueDiffWithinAt 𝕜 (s ∩ t) x
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.ofNNReal_finsuppProd : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] (f : ι →₀ M) (g : ι → M → NNReal),
  ↑(f.prod g) = f.prod fun i m => ↑(g i m)
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- **Alias** of `Nat.infinite_setOfPred_prime_and_modEq`. -/
Nat.infinite_setOf_prime_and_modEq : ∀ {q a : ℕ}, q ≠ 0 → a.Coprime q → {p | Nat.Prime p ∧ p ≡ a [MOD q]}.Infinite
-- Mathlib.Order.Filter.ENNReal
ENNReal.limsup_const_mul_of_ne_top : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal},
  a ≠ ⊤ → Filter.limsup (fun x => a * u x) f = a * Filter.limsup u f
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- A chosen left adjoint to a functor that is a right adjoint.  -/
CategoryTheory.Functor.leftAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) → [R.IsRightAdjoint] → CategoryTheory.Functor C D
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of a coherence isomorphism.  -/
Mathlib.Tactic.BicategoryLike.CoherenceHom.src : Mathlib.Tactic.BicategoryLike.CoherenceHom → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_coe : ∀ (θ : ℝ), (↑θ).toReal = toIocMod Real.two_pi_pos (-Real.pi) θ
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The underlying ideal.  -/
DividedPowers.SubDPIdeal.carrier : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → hI.SubDPIdeal → Ideal A
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat.div_of_dvd : ∀ {p a b : ℕ} [hp : Fact (Nat.Prime p)], b ∣ a → padicValNat p (a / b) = padicValNat p a - padicValNat p b
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The category instance.  -/
Mathlib.Tactic.Monoidal.Context.instCat : (self : Mathlib.Tactic.Monoidal.Context) → Q(CategoryTheory.Category.{udummy._pp_uniq.3, udummy._pp_uniq.4} unknown_1)
-- Mathlib.Order.UpperLower.Basic
OrderEmbedding.image_Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β),
  IsUpperSet (Set.range ⇑e) → ∀ (a : α), ⇑e '' Set.Ioi a = Set.Ioi (e a)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
PiToModule.fromMatrix_apply : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) [inst_4 : DecidableEq ι] (A : Matrix ι ι R) (w : ι → R),
  ((PiToModule.fromMatrix R b) A) w = (Fintype.linearCombination R b) (A.mulVec w)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.TensorProduct.map_map_comp_assoc_symm_eq_assoc : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15}
  {N₃ : Type u_16} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid N₁] [inst_7 : AddCommMonoid N₂]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] [inst_13 : Module R N₂] [inst_14 : Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂)
  (f₃ : M₃ →ₗ[R] N₃) (f : M →ₗ[R] TensorProduct R M₁ (TensorProduct R M₂ M₃)),
  TensorProduct.map (TensorProduct.map f₁ f₂) f₃ ∘ₗ ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ f =
    ↑(TensorProduct.assoc R N₁ N₂ N₃).symm ∘ₗ TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ f
-- Init.Data.Array.Attach
Array.attachWith_empty : ∀ {α : Type u_1} {P : α → Prop} (H : ∀ x ∈ #[], P x), #[].attachWith P H = #[]
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.carrier_eq_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α), s.carrier = ↑s
-- Mathlib.Data.ZMod.Basic
/-- Equivalence between the units of `ZMod n` and
the subtype of terms `x : ZMod n` for which `x.val` is coprime to `n`  -/
ZMod.unitsEquivCoprime : {n : ℕ} → [NeZero n] → (ZMod n)ˣ ≃ { x // x.val.Coprime n }
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.ker_evalₗ : ∀ (σ K : Type u) [inst : Fintype K] [inst_1 : Field K] [Finite σ], (MvPolynomial.evalᵢ σ K).ker = ⊥
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom.eq_1 : ∀ (g : GL (Fin 2) ℝ) (z : ℂ), UpperHalfPlane.denom g z = ↑(↑g 1 0) * z + ↑(↑g 1 1)
-- Std.Data.DHashMap.Basic
/-- Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof
of `a ∈ m`.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.get : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → (m : Std.DHashMap α β) → (a : α) → a ∈ m → β a
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.mk_eq_mk_iff : ∀ {α : Type u_2} {rels : FreeMonoid α → FreeMonoid α → Prop} {x y : FreeMonoid α},
  (PresentedMonoid.mk rels) x = (PresentedMonoid.mk rels) y ↔ (conGen rels) x y
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The zeroth coefficient of the `q`-expansion of a cusp form vanishes.  -/
CuspFormClass.qExpansion_coeff_zero : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [CuspFormClass F Γ k], 0 < h → h ∈ Γ.strictPeriods → (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h ⇑f) = 0
-- Lean.Environment
Lean.instDecidableEqOLeanLevel : DecidableEq Lean.OLeanLevel
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFoldr.congr_simp : ∀ {α : Type u_3} {β : Type u_4} (f f_1 : α → β → β) (e_f : f = f_1) (s s_1 : Multiset α) (e_s : s = s_1)
  (comm : {x | x ∈ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)) (b b_1 : β),
  b = b_1 → Multiset.noncommFoldr f s comm b = Multiset.noncommFoldr f_1 s_1 ⋯ b_1
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_ne_one : ∀ {x : ENNReal}, ↑x ≠ 1 ↔ x ≠ 1
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_toUInt16 : ∀ (n : USize) (h : System.Platform.numBits = 32), n.toUInt16.toBitVec = BitVec.setWidth 16 (n.toBitVec32 h)
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.mk.inj : ∀ {X : Type u} {Y : Type v} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} {toFun : C(X, Y)}
  {invFun : C(Y, X)} {left_inv : (invFun.comp toFun).Homotopic (ContinuousMap.id X)}
  {right_inv : (toFun.comp invFun).Homotopic (ContinuousMap.id Y)} {toFun_1 : C(X, Y)} {invFun_1 : C(Y, X)}
  {left_inv_1 : (invFun_1.comp toFun_1).Homotopic (ContinuousMap.id X)}
  {right_inv_1 : (toFun_1.comp invFun_1).Homotopic (ContinuousMap.id Y)},
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 } →
    toFun = toFun_1 ∧ invFun = invFun_1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.comp_mapAddGrp_zero_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (A : CategoryTheory.AddGrp C) {Z : E} (h : ((F.comp G).mapAddGrp.obj A).X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G))
        (G.map (F.map CategoryTheory.AddMonObj.zero)))
      h
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.newGoal? : Aesop.NormRuleResult → Option Lean.MVarId
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind_comp_friend_left.match_1_1.eq_1 : ∀ {α : Type u_1} (motive : (Stream'.Seq α → Stream'.Seq α) → Prop)
  (motive_1 : Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation × Subtype motive) → Sort u_2)
  (h_1 : Unit → motive_1 none)
  (h_2 :
    (hd : α) →
      (opf' : Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) →
        (op' : Subtype motive) → motive_1 (some (hd, opf', op'))),
  (match none with
    | none => h_1 ()
    | some (hd, opf', op') => h_2 hd opf' op') =
    h_1 ()
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.wordProd_cons : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω : List B),
  cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : E.X i' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).inv
      (CategoryTheory.CategoryStruct.comp (E.p₁ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k)) h) =
    CategoryTheory.CategoryStruct.comp (E.p₁ k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
-- Mathlib.Order.Hom.Lattice
InfHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] {f g : InfHom α β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Data.W.Constructions
WType.instInhabitedNatβSucc : Inhabited (WType.Natβ WType.Natα.succ)
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsTransitive.subset_of_mem : ∀ {x y : ZFSet.{u}}, x.IsTransitive → y ∈ x → y ⊆ x
-- Init.Core
imp_congr_right : ∀ {a b c : Prop}, (a → (b ↔ c)) → (a → b ↔ a → c)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {e f : C ≌ D} {α β : e ⟶ f}, α = β ↔ CategoryTheory.Equivalence.asNatTrans α = CategoryTheory.Equivalence.asNatTrans β
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InsertReplaceEdit.mk.sizeOf_spec : ∀ (newText : String) (insert replace : Lean.Lsp.Range),
  sizeOf { newText := newText, insert := insert, replace := replace } =
    1 + sizeOf newText + sizeOf insert + sizeOf replace
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EST.bind.match_1.eq_2 : ∀ {ε σ α : Type} (motive : EST.Out ε σ α → Sort u_1) (e : ε) (s : Void σ)
  (h_1 : (a : α) → (s : Void σ) → motive (EST.Out.ok a s)) (h_2 : (e : ε) → (s : Void σ) → motive (EST.Out.error e s)),
  (match EST.Out.error e s with
    | EST.Out.ok a s => h_1 a s
    | EST.Out.error e s => h_2 e s) =
    h_2 e s
-- Mathlib.Order.Disjoint
Complementeds.isCompl_coe : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b : Complementeds α},
  IsCompl ↑a ↑b ↔ IsCompl a b
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.TextDocumentClientCapabilities.inlayHint? : Lean.Lsp.TextDocumentClientCapabilities → Option Lean.Lsp.InlayHintClientCapabilities
-- Mathlib.Algebra.Group.Basic
eq_of_sub_eq_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a - b = 0 → a = b
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalCategoryMop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.MonoidalCategory Cᴹᵒᵖ
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.recvSelector.registerAux : {α : Type} → Std.Bounded.Receiver✝ α → Std.Async.Waiter (Option α) → IO Unit
-- Mathlib.Analysis.Normed.Module.Basic
dist_algebraMap : ∀ {𝕜 : Type u_1} (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  (x y : 𝕜), dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y * ‖1‖
-- Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
/-- A C⋆-algebra is spanned by nonnegative elements of norm at most `r`  -/
CStarAlgebra.span_nonneg_inter_closedBall : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {r : ℝ},
  0 < r → Submodule.span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 r) = ⊤
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.coe_mk : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : ((i : ι) → M₁ i) → M₂)
  (h₁ :
    ∀ [inst : 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))
  (h₂ :
    ∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
      f (Function.update m i (c • x)) = c • f (Function.update m i x)),
  ⇑{ toFun := f, map_update_add' := h₁, map_update_smul' := h₂ } = f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.inv` -/
MeasureTheory.AEStronglyMeasurable.fun_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Inv β] [ContinuousInv β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun i => (f i)⁻¹) μ
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.mk : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        {φ : R →* S} →
          {A : Type v} →
            {B : Type w} →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] →
                    [inst_5 : DistribMulAction S B] →
                      (toDistribMulActionHom : A →ₑ+[φ] B) →
                        (∀ (x y : A),
                            toDistribMulActionHom.toFun (x * y) =
                              toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y) →
                          A →ₛₙₐ[φ] B
-- Init.Data.List.Count
List.length_eq_countP_add_countP : ∀ {α : Type u_1} (p : α → Bool) {l : List α}, l.length = List.countP p l + List.countP (fun a => decide ¬p a = true) l
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F},
  ContDiffAt 𝕜 (↑n) f x → ContDiffAt 𝕜 (↑n) g x → iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- An action is preprimitive if it is pretransitive and
the only blocks are the trivial ones  -/
MulAction.IsPreprimitive.isTrivialBlock_of_isBlock : ∀ {G : Type u_1} {X : Type u_2} {inst : SMul G X} [self : MulAction.IsPreprimitive G X] {B : Set X},
  MulAction.IsBlock G B → MulAction.IsTrivialBlock B
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.zero : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.Kernel.HasSubgaussianMGF 0 0 κ ν
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.eq_bot_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L),
  K = ⊥ ↔ ∀ x ∈ K, x = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_eq_pi_div_four : ∀ {x : ℝ}, Real.arctan x = Real.pi / 4 ↔ x = 1
-- Lean.Parser.Syntax
Lean.Parser.Syntax.sepBy1 : Lean.Parser.Parser
-- Mathlib.Algebra.Lie.Basis.Prod
/-- The equivalence obtained by interchanging the two bases consumed by `LieAlgebra.Basis.prod`.  -/
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodSymmEquiv : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {R : Type u_5} →
                    [inst_4 : CommRing R] →
                      [inst_5 : LieAlgebra R L₁] →
                        {H₁ : LieSubalgebra R L₁} →
                          (b₁ : LieAlgebra.Basis ι₁ H₁) →
                            [inst_6 : LieAlgebra R L₂] →
                              {H₂ : LieSubalgebra R L₂} →
                                (b₂ : LieAlgebra.Basis ι₂ H₂) →
                                  ↥(LieAlgebra.Basis.prod✝ eι.symm b₂ b₁) ≃ₗ⁅R⁆ ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂)
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_mul_right : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a : α}, IsUnit a → ∀ (b : α), a / (a * b) = 1 / b
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Turn minimal axioms for `CompletelyDistribLattice` into minimal axioms for
`CompleteDistribLattice`.  -/
CompletelyDistribLattice.MinimalAxioms.toCompleteDistribLattice : ∀ {α : Type u} [inst : CompleteLattice α],
  CompletelyDistribLattice.MinimalAxioms α → CompleteDistribLattice.MinimalAxioms α
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The preimage of a set `s` under a continuous linear map `f` with nonzero determinant has measure
equal to `μ s` times the absolute value of the inverse of the determinant of `f`.  -/
MeasureTheory.Measure.addHaar_preimage_continuousLinearMap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E →L[ℝ] E},
  LinearMap.det ↑f ≠ 0 → ∀ (s : Set E), μ (⇑f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det ↑f)⁻¹| * μ s
-- Mathlib.Tactic.Linter.PPRoundtrip
/-- `posToShiftedPos lths diff` takes as input an array `lths` of natural numbers,
and one further natural number `diff`.
It adds up the elements of `lths` occupying the odd positions, as long as the sum of the
elements in the even positions does not exceed `diff`.
It returns the sum of the accumulated odds and `diff`.
This is useful to figure out the difference between the output of `polishSource s` and `s` itself.
It plays a role similar to the `fileMap`.  -/
_private.Mathlib.Tactic.Linter.PPRoundtrip.0.Mathlib.Linter.posToShiftedPos : Array ℕ → ℕ → ℕ
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.modByMonicHom_root_pow : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) {n : ℕ}, n < f.natDegree → h.modByMonicHom (h.root ^ n) = Polynomial.X ^ n
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.singleton_apply : ∀ (ι : Type u_7) (R : Type u_8) [inst : Unique ι] [inst_1 : Semiring R] (i : ι), (Module.Basis.singleton ι R) i = 1
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_ne_zero_iff : ∀ {n : ℕ}, ArithmeticFunction.vonMangoldt n ≠ 0 ↔ IsPrimePow n
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- The basis of `ZLattice.comap K L e` given by the image of a basis `b` of `L` by `e.symm`.  -/
Module.Basis.ofZLatticeComap : (K : Type u_1) →
  [inst : NormedField K] →
    {E : Type u_2} →
      {F : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace K F] →
                (L : Submodule ℤ E) →
                  (e : F ≃ₗ[K] E) → {ι : Type u_4} → Module.Basis ι ℤ ↥L → Module.Basis ι ℤ ↥(ZLattice.comap K L ↑e)
-- Init.Data.Float.Float
/-- Computes the base-2 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`log2`.
 -/
Float.log2 : Float → Float
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.unop : C ⥤ D` preserves
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.preservesColimit_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimit K.op F],
  CategoryTheory.Limits.PreservesColimit K F.unop
-- Mathlib.Topology.ContinuousOn
ContinuousOn.continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousOn f s → s ∈ nhds x → ContinuousAt f x
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.copy_eq : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : α → α) (h : f' = ⇑f), f.copy f' h = f
-- Std.Do.SPred.Notation
/-- Bi-entailment in `SPred`; sugar for `SPred.bientails`.  -/
Std.Do.«term_⊣⊢ₛ_» : Lean.TrailingParserDescr
-- Mathlib.Data.Int.GCD
Commute.pow_eq_pow_iff_of_coprime : ∀ {α : Type u_1} [inst : GroupWithZero α] {a b : α} {m n : ℕ},
  Commute a b → m.Coprime n → (a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m)
-- Mathlib.Topology.DiscreteSubset
/-- A set `s` is codiscrete within `U` iff `s ∪ Uᶜ` is a punctured neighborhood of every point in `U`.
 -/
mem_codiscreteWithin_iff_forall_mem_nhdsNE : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S T : Set X},
  S ∈ Filter.codiscreteWithin T ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ nhdsWithin x {x}ᶜ