mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Associator
Equiv.tensorProductAssoc_def : ∀ (R : Type u_11) {A : Type u_12} {A' : Type u_13} {B : Type u_14} {B' : Type u_15} {C : Type u_16} {C' : Type u_17}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid A'] [inst_2 : AddCommMonoid B'] [inst_3 : AddCommMonoid C']
  [inst_4 : Module R A'] [inst_5 : Module R B'] [inst_6 : Module R C'] (eA : A ≃ A') (eB : B ≃ B') (eC : C ≃ C'),
  TensorProduct.assoc R A B C =
    TensorProduct.congr (TensorProduct.congr (Equiv.linearEquiv R eA) (Equiv.linearEquiv R eB))
        (Equiv.linearEquiv R eC) ≪≫ₗ
      (TensorProduct.assoc R A' B' C' ≪≫ₗ
        TensorProduct.congr (Equiv.linearEquiv R eA).symm
          (TensorProduct.congr (Equiv.linearEquiv R eB).symm (Equiv.linearEquiv R eC).symm))
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instContinuousSMul : ∀ (R : Type u_1) {A : Type u_3} {E : Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace R]
  [inst_2 : AddCommGroup E] [inst_3 : UniformSpace E] [inst_4 : Module R E] [ContinuousSMul R E],
  ContinuousSMul R (WithCStarModule A E)
-- Mathlib.Algebra.Group.Submonoid.Finsupp
AddSubmonoid.exists_of_mem_closure_range : ∀ {M : Type u_1} [inst : AddCommMonoid M] {ι : Type u_2} (f : ι → M) (x : M) [inst_1 : Fintype ι],
  x ∈ AddSubmonoid.closure (Set.range f) → ∃ a, x = ∑ i, a i • f i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_eq : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α} (h' : k ∈ m), m.getKey k h' = k
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
/-- The derivative of the `Γ` integral, at any `s ∈ ℂ` with `1 < re s`, is given by the Mellin
transform of `log t * exp (-t)`.  -/
Complex.hasDerivAt_GammaIntegral : ∀ {s : ℂ},
  0 < s.re →
    HasDerivAt Complex.GammaIntegral (∫ (t : ℝ) in Set.Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(Real.exp (-t)))) s
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Purity.ofNat : ℕ → Lean.Compiler.LCNF.Purity
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).contains k = true
-- Init.Data.Ord.Basic
List.compareLex_nil_right_eq_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {xs : List α}, List.compareLex cmp xs [] = Ordering.eq ↔ xs = []
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_def : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f),
  h.algEquiv h' = h.adjoinRootAlgEquiv.symm.trans h'.adjoinRootAlgEquiv
-- Mathlib.Topology.Instances.ENat
Filter.Tendsto.enatSub : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℕ∞} {a b : ℕ∞},
  Filter.Tendsto f l (nhds a) →
    Filter.Tendsto g l (nhds b) → a ≠ ⊤ ∨ b ≠ ⊤ → Filter.Tendsto (fun x => f x - g x) l (nhds (a - b))
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.runM : {α : Type} → Lean.Environment → Lean.CollectAxioms.M✝ α → α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G),
  CochainComplex.HomComplex.Cochain.ofHom (φ₁ - φ₂) =
    CochainComplex.HomComplex.Cochain.ofHom φ₁ - CochainComplex.HomComplex.Cochain.ofHom φ₂
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- The `n`th elementary symmetric `MvPolynomial σ R` is obtained by evaluating the
`n`th elementary symmetric at the `Multiset` of the monomials  -/
MvPolynomial.esymm_eq_multiset_esymm : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ],
  MvPolynomial.esymm σ R = (Multiset.map MvPolynomial.X Finset.univ.val).esymm
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.match_1.congr_eq_2 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  x = Ordering.eq →
    (match x with
      | Ordering.lt => h_1 ()
      | Ordering.eq => h_2 ()
      | Ordering.gt => h_3 ()) ≍
      h_2 ()
-- Mathlib.GroupTheory.Nilpotent
Subgroup.mem_upperCentralSeriesStep : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [inst_1 : N.Normal] (x : G),
  x ∈ N.upperCentralSeriesStep ↔ ∀ (y : G), ⁅x, y⁆ ∈ N
-- Mathlib.CategoryTheory.MorphismProperty.IsSmall
/-- A class of morphisms `W : MorphismProperty C` is `w`-small
if the corresponding set in `Set (Arrow C)` is.  -/
CategoryTheory.MorphismProperty.IsSmall : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G],
  LinearMapClass (LeftInvariantDerivation I G) 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
    (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddAbove.range_neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {α : Type u_4} {f : α → G},
  BddAbove (Set.range f) → BddBelow (Set.range fun x => -f x)
-- Init.Data.List.Lex
List.lex.eq_def : ∀ {α : Type u} [inst : BEq α] (l₁ l₂ : List α) (lt : α → α → Bool),
  l₁.lex l₂ lt =
    match l₁, l₂ with
    | [], head :: tail => true
    | x, [] => false
    | a :: as, b :: bs => lt a b || a == b && as.lex bs lt
-- Batteries.Data.List.Lemmas
List.disjoint_of_disjoint_cons_left : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Disjoint l₂ → l₁.Disjoint l₂
-- Mathlib.Analysis.Polynomial.Fourier
Polynomial.toAddCircle_monomial_eq_smul_fourier : ∀ {n : ℕ} {c : ℂ}, Polynomial.toAddCircle ((Polynomial.monomial n) c) = c • fourier ↑n
-- Lean.Elab.InfoTree.Types
Lean.Elab.UserWidgetInfo.mk : Lean.Widget.WidgetInstance → Lean.Syntax → Lean.Elab.UserWidgetInfo
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link2.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3) →
      (r : Std.DTreeMap.Internal.Impl α β) →
        (hr : r.Balanced) →
          ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
              r = Std.DTreeMap.Internal.Impl.leaf → motive Std.DTreeMap.Internal.Impl.leaf hr) →
            ((szr : ℕ) →
                (k'' : α) →
                  (v'' : β k'') →
                    (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
                      (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) →
                        r = Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' →
                          motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') hr) →
              motive r hr
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousWithinAt.zsmul : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α} {s : Set α},
  ContinuousWithinAt f s x → ∀ (z : ℤ), ContinuousWithinAt (z • f) s x
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- A subgroup of a seminormed group is also a seminormed group, with the restriction
of the norm.  -/
AddSubgroup.seminormedAddGroup : {E : Type u_1} → [inst : SeminormedAddGroup E] → {s : AddSubgroup E} → SeminormedAddGroup ↥s
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.equivInfinitePlace.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  NumberField.IsCMField.equivInfinitePlace K = NumberField.IsCMField.equivInfinitePlace K
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The witness that each `X : FormalCoproduct.{w} C` is itself a coproduct of objects of the
original category (after coercion using `incl C`), specified by `X.toFun`.  -/
CategoryTheory.Limits.FormalCoproduct.cofanPtIsoSelf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.Limits.FormalCoproduct C) → (CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).pt ≅ X
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.toLaxRightLinear : {D : Type u_1} →
  {D' : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} D} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C} →
              {inst_3 : CategoryTheory.MonoidalCategory C} →
                {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D} →
                  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} →
                    [self : F.RightLinear C] → F.LaxRightLinear C
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceWaitForDiagnosticsParams : Lean.Lsp.FileSource Lean.Lsp.WaitForDiagnosticsParams
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.idealOfVars_eq_restrictSupportIdeal : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R],
  MvPolynomial.idealOfVars σ R = MvPolynomial.restrictSupportIdeal R (⇑Finsupp.degree ⁻¹' Set.Ici 1) ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_inter_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.expPartialHomeomorph_symm_apply : ∀ (x : ℝ), ↑Real.expPartialHomeomorph.symm x = Real.log x
-- Mathlib.Algebra.Ring.Equiv
/-- makes a `NonUnitalRingHom` from the bijective inverse of a `NonUnitalRingHom`  -/
NonUnitalRingHom.inverse : {R : Type u_4} →
  {S : Type u_5} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] →
        (f : R →ₙ+* S) → (g : S → R) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → S →ₙ+* R
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- Auxiliary construction for `lift`.  -/
CategoryTheory.ProjectiveResolution.liftFZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Y Z : C} →
          (Y ⟶ Z) →
            (P : CategoryTheory.ProjectiveResolution Y) →
              (Q : CategoryTheory.ProjectiveResolution Z) → P.complex.X 0 ⟶ Q.complex.X 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMapM_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.mapM f it)).toList =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          g __do_lift)
        it).toList
-- Mathlib.Algebra.Group.Units.Defs
/-- Multiplication by a `u : Mˣ` on the right doesn't affect `IsUnit`.  -/
Units.isUnit_mul_units : ∀ {M : Type u_1} [inst : Monoid M] (a : M) (u : Mˣ), IsUnit (a * ↑u) ↔ IsUnit a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.max? = some km → t.get? km = some km
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.symm : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a }),
  Equiv.symm (ep.subtypeCongr en) = Equiv.Perm.subtypeCongr (Equiv.symm ep) (Equiv.symm en)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.get_dmap : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : (a : α) → x = some a → β}
  (h : (Std.Internal.List.Option.dmap✝ x f).isSome = true), (Std.Internal.List.Option.dmap✝ x f).get h = f (x.get ⋯) ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The connected component of a `0`-simplex of a simplicial set.  -/
SSet.π₀.mk : {X : SSet} → X.obj (Opposite.op { len := 0 }) → X.π₀
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.obj X).right =
    X.obj (Opposite.op CategoryTheory.WithInitial.star)
-- Lean.Meta.HaveTelescope
Lean.Meta.instInhabitedHaveTelescopeInfo : Inhabited Lean.Meta.HaveTelescopeInfo
-- Std.Internal.Do.Order.PreservesSup
/-- Monotonicity of a `Sup`-preserving `f`, derived from join preservation.  -/
Lean.Order.PreservesSup.map_mono : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (f : α → α) [Lean.Order.PreservesSup f] {b b' : α},
  Lean.Order.PartialOrder.rel b b' → Lean.Order.PartialOrder.rel (f b) (f b')
-- Mathlib.Algebra.Order.Group.End
RelEmbedding.coe_mul : ∀ {α : Type u_1} {r : α → α → Prop} (f g : r ↪r r), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Rel.brecOn : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop}
  {motive : (a : Multiset α) → (a_1 : Multiset β) → Multiset.Rel r a a_1 → Prop} {a : Multiset α} {a_1 : Multiset β}
  (t : Multiset.Rel r a a_1),
  (∀ (a : Multiset α) (a_2 : Multiset β) (t : Multiset.Rel r a a_2), Multiset.Rel.below t → motive a a_2 t) →
    motive a a_1 t
-- Init.Data.Nat.Dvd
Nat.dvd_iff_mod_eq_zero : ∀ {m n : ℕ}, m ∣ n ↔ n % m = 0
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.atom_pf : ∀ {R : Type u_1} [inst : CommSemiring R] {b : R} (a : R) {e : ℕ},
  Nat.rawCast 1 = e → a ^ e * Nat.rawCast 1 = b → a = b + 0
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_iUnion : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {δ : Type u_7} (s : δ → Set α), Finsupp.supported M R (⋃ i, s i) = ⨆ i, Finsupp.supported M R (s i)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.eq_1 : ∀ (coeff k : ℤ),
  Int.Internal.Linear.Expr.toPoly'.go coeff (Int.Internal.Linear.Expr.num k) =
    bif k == 0 then id else fun x => x.addConst (coeff.mul k)
-- Mathlib.Order.Hom.Set
Set.MapsTo.sumElim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} {s : Set α × Set β} {t : Set γ},
  Set.MapsTo f s.1 t → Set.MapsTo g s.2 t → Set.MapsTo (Sum.elim f g) (Set.sumEquiv.symm s) t
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
Continuous.map_borel_eq : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [PolishSpace X] [inst_2 : TopologicalSpace Y] [T0Space Y]
  [SecondCountableTopology Y] {f : X → Y},
  Continuous f → Function.Surjective f → MeasurableSpace.map f (borel X) = borel Y
-- Mathlib.Algebra.Order.Monovary
antivaryOn_inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → (AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_one : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M], MonoidHom.ker 1 = ⊤
-- Mathlib.Order.RelIso.Basic
RelIso.embeddingSurjectiveEquivIso_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : { f // Function.Surjective ⇑f }),
  RelIso.embeddingSurjectiveEquivIso f = RelIso.ofSurjective ↑f ⋯
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.toAddSubmonoid_injective : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], Function.Injective NonUnitalSubsemiring.toAddSubmonoid
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α], Topology.IsEmbedding TopologicalSpace.NonemptyCompacts.toCompacts
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.mapMulHom_injective : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] {f : α →ₙ* β},
  Function.Injective ⇑f → Function.Injective ⇑(WithOne.mapMulHom f)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNatAux.eq_1 : ∀ (b q : ℕ), LucasLehmer.norm_num_ext.sModNatAux b q 0 = b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : β k → β k},
      Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.modify k f t) =
        Std.DTreeMap.Internal.Impl.contains k' t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α}, ∅.getKey? a = none
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsDetecting.isIso_iff_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsDetecting →
    ∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
      CategoryTheory.IsIso f ↔
        ∀ (G : C),
          P G →
            Function.Surjective
              ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyoneda.obj (Opposite.op G)).map f))
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- A homotopy of refinements `E ⟶ F` is a family of morphisms `Xᵢ ⟶ Yₐ` where
`Yₐ` is a component of the cover of `X_{f(i)} ×[S] X_{g(i)}`.  -/
CategoryTheory.PreOneHypercover.Homotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} → E.Hom F → E.Hom F → Type (max (max v w) w')
-- Mathlib.Data.Rat.Defs
Rat.natCast_injective : Function.Injective Nat.cast
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_mul : ∀ {ι : Type u_1} {M : Type u_4} [inst : Semiring M] [inst_1 : Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] (s : Finset ι)
  (f : ι → M) (a : M), (s.expect fun i => f i) * a = s.expect fun i => f i * a
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_iUnion₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set β} {f : α → β},
  Set.MapsTo f (⋃ i, ⋃ j, s i j) t ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t
-- Mathlib.FieldTheory.Fixed
/-- The subfield of fixed points by a monoid action.  -/
FixedPoints.subfield : (M : Type u) → [inst : Monoid M] → (F : Type v) → [inst_1 : Field F] → [MulSemiringAction M F] → Subfield F
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.isStableUnderColimitsOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{w, w', v, u} W] (J : Type w')
  [inst_1 : CategoryTheory.Category.{w, w'} J] [CategoryTheory.IsFiltered J], W.IsStableUnderColimitsOfShape J
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatch_of_ofSliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {pos : (s.sliceFrom p).Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat (String.Slice.Pos.ofSliceFrom pos) →
    String.Slice.Pattern.Model.IsLongestRevMatch pat pos
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f (CategoryTheory.CategoryStruct.comp g g'))
      (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv =
    CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushout.inr f g) g'
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instCoeSubgroup : {G : Type u_1} → [inst : Group G] → Coe (FiniteIndexNormalSubgroup G) (Subgroup G)
-- Mathlib.GroupTheory.Sylow
/-- The preimage of a Sylow subgroup under an injective homomorphism is a Sylow subgroup.  -/
Sylow.comapOfInjective : {p : ℕ} →
  {G : Type u_1} →
    [inst : Group G] →
      (P : Sylow p G) →
        {K : Type u_2} → [inst_1 : Group K] → (ϕ : K →* G) → Function.Injective ⇑ϕ → ↑P ≤ ϕ.range → Sylow p K
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
trdeg_subsingleton : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Subsingleton R],
  Algebra.trdeg R A = 1
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- A general form of Möbius inversion. Based on lemma 2.1.3 of Incidence Algebras by Spiegel and
O'Donnell.  -/
IncidenceAlgebra.moebius_inversion_bot : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : OrderBot α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (f g : α → 𝕜),
  (∀ (x : α), g x = ∑ y ≤ x, f y) → ∀ (x : α), f x = ∑ y ≤ x, (IncidenceAlgebra.mu 𝕜) y x * g y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.mul_cert.eq_1 : ∀ (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.mul_cert p₁ k p = (Lean.Grind.CommRing.Poly.mulConst_k k p₁).beq' p
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSlice : (α : Type u_1) → (α → Type u_2) → [Ord α] → Type (max u_2 u_1)
-- Mathlib.LinearAlgebra.Matrix.WithConv
WithConv.matrixToLin'StarAlgEquiv_apply : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : CommSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (x : WithConv (Matrix m n α)),
  (WithConv.matrixToLin'StarAlgEquiv m n α) x = WithConv.toConv (Matrix.toLin' x.ofConv)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- The conjugation action by elements of the spin group keeps vectors as vectors.  -/
spinGroup.conjAct_smul_ι_mem_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  ↑x ∈ spinGroup Q →
    ∀ [Invertible 2] (y : M), ConjAct.toConjAct x • (CliffordAlgebra.ι Q) y ∈ (CliffordAlgebra.ι Q).range
-- Init.Meta.Defs
/-- Configures the behavior of the `rewrite` and `rw` tactics.  -/
Lean.Meta.Rewrite.Config : Type
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.isSheaf : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A),
  CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf data G₀)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instHasInitialScheme : CategoryTheory.Limits.HasInitial AlgebraicGeometry.Scheme