mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapᵣ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapᵣ F).app X =
    F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.RepresentationTheory.Intertwining
/-- The kernel of an intertwining map from `V` to `W` as a subrepresentation of `V`.  -/
Representation.IntertwiningMap.ker : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → ρ.IntertwiningMap σ → Subrepresentation ρ
-- Mathlib.Algebra.Star.StarAlgHom
/-- If `A₁` is equivalent to `A₁'` and `A₂` is equivalent to `A₂'` as star algebras, then the type
of maps `A₁ →⋆ₙₐ[R] A₂` is equivalent to the type of maps `A₁' →⋆ₙₐ[R] A₂'`.

For unital star algebra homomorphisms, see `StarAlgEquiv.arrowCongr`.  -/
StarAlgEquiv.arrowCongr' : {R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      {A₁' : Type u_5} →
        {A₂' : Type u_6} →
          [inst : Monoid R] →
            [inst_1 : NonUnitalNonAssocSemiring A₁] →
              [inst_2 : DistribMulAction R A₁] →
                [inst_3 : Star A₁] →
                  [inst_4 : NonUnitalNonAssocSemiring A₂] →
                    [inst_5 : DistribMulAction R A₂] →
                      [inst_6 : Star A₂] →
                        [inst_7 : NonUnitalNonAssocSemiring A₁'] →
                          [inst_8 : DistribMulAction R A₁'] →
                            [inst_9 : Star A₁'] →
                              [inst_10 : NonUnitalNonAssocSemiring A₂'] →
                                [inst_11 : DistribMulAction R A₂'] →
                                  [inst_12 : Star A₂'] →
                                    (A₁ ≃⋆ₐ[R] A₁') → (A₂ ≃⋆ₐ[R] A₂') → (A₁ →⋆ₙₐ[R] A₂) ≃ (A₁' →⋆ₙₐ[R] A₂')
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.commGroupObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommGrpCat) → (j : J) → CommGroup ((F.comp (CategoryTheory.forget CommGrpCat)).obj j)
-- Batteries.Control.LawfulMonadState
/-- Setting and then returning the monad state is the same as returning the set value.  -/
LawfulMonadStateOf.set_bind_get : ∀ {σ : semiOutParam (Type u_1)} {m : Type u_1 → Type u_2} {inst : Monad m} {inst_1 : MonadStateOf σ m}
  [self : LawfulMonadStateOf σ m] (s : σ),
  (do
      set s
      get) =
    do
    set s
    pure s
-- Mathlib.Order.Bounds.Image
IsGreatest.isGreatest_image2_of_isLeast : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → IsGreatest s a → IsLeast t b → IsGreatest (Set.image2 f s t) (f a b)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ext_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {x y : PolynomialModule R M}, x = y ↔ x.coeff = y.coeff
-- Std.Data.DTreeMap.Basic
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.DTreeMap.union : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp
-- Mathlib.RingTheory.KrullDimension.Basic
/-- Alternative constructor for `Ring.KrullDimLE 1`, convenient for domains.  -/
Ring.KrullDimLE.mk₁' : ∀ {R : Type u_1} [inst : CommSemiring R], (∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal) → Ring.KrullDimLE 1 R
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ico_add_one_left_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a b : α},
  a < b → insert a (Set.Ico (a + 1) b) = Set.Ico a b
-- Mathlib.Analysis.Seminorm
Seminorm.neg_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (r : ℝ) (x : E), -p.ball x r = p.ball (-x) r
-- Mathlib.Order.WithBotTop
WithBotTop.instCoe : {ι : Type u_1} → Coe ι (WithBotTop ι)
-- Init.Data.SInt.Bitwise
Int64.or_self : ∀ {a : Int64}, a ||| a = a
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.minimalPeriod_dvd : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x → Function.minimalPeriod f x ∣ n
-- Mathlib.Analysis.Normed.Group.Int
norm_zpow_le_mul_norm : ∀ {α : Type u_1} [inst : SeminormedCommGroup α] (n : ℤ) (a : α), ‖a ^ n‖ ≤ ‖n‖ * ‖a‖
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.mk_vadd : ∀ {M' : Type u_1} {α : Type u_2} [inst : AddZeroClass M'] [inst_1 : VAdd M' α] {S : AddSubmonoid M'} (g : M')
  (hg : g ∈ S) (a : α), ⟨g, hg⟩ +ᵥ a = g +ᵥ a
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.instFunLike : {α : Type u_1} → [inst : MeasurableSpace α] → FunLike (MeasureTheory.Measure α) (Set α) ENNReal
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.trans_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  {f₀ f₁ f₂ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (G : f₁.HomotopyWith f₂ P) (x : ↑unitInterval × X),
  (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {fallback : α}, t.getKey! (t.minKeyD fallback) = t.minKeyD fallback
-- Init.Meta.Defs
Lean.MonadNameGenerator.getNGen : {m : Type → Type} → [self : Lean.MonadNameGenerator m] → m Lean.NameGenerator
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measurableSet_sigmaFiniteSetWRT' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure ν],
  MeasurableSet (μ.sigmaFiniteSetWRT' ν)
-- Init.Data.Int.DivMod.Pow
_private.Init.Data.Int.DivMod.Pow.0.Int.dvd_pow : ∀ {a b : ℤ} {n : ℕ}, b ∣ a → b ^ n ∣ a ^ n
-- Init.Data.List.Monadic
List.foldlM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {xs : List α} {f : β → α → m β} {init : β},
  List.foldlM f init (wfParam xs) = List.foldlM f init xs.attach.unattach
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeRightOp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp),
  CategoryTheory.Limits.coconeOfConeRightOp c =
    { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.removeRightOp c.π }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_insertMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α}, k ∈ ↑(t.insertMany! l) → (List.map Sigma.fst l).contains k = false → k ∈ t
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.subLeft_symm_apply : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G]
  [inst_3 : IsIsometricVAdd Gᵃᵒᵖ G] (c b : G), (IsometryEquiv.subLeft c).symm b = -b + c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tendsto_arctan_atBot : Filter.Tendsto Real.arctan Filter.atBot (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2))))
-- Mathlib.Data.Rel
SetRel.prod_comp_prod_of_disjoint : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t₁ t₂ : Set β},
  Disjoint t₁ t₂ → ∀ (s : Set α) (u : Set γ), SetRel.comp (s ×ˢ t₁) (t₂ ×ˢ u) = ∅
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_3),
  (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Computability.EpsilonNFA
εNFA.accept_one : ∀ {α : Type u} {σ : Type v}, εNFA.accept 1 = Set.univ
-- Lean.Elab.PatternVar
/-- Pattern variables found so far.  -/
Lean.Elab.Term.CollectPatternVars.State.found : Lean.Elab.Term.CollectPatternVars.State → Lean.NameSet
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Finset.norm_prod_one_add_sub_one_le : ∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] (t : Finset ι) (f : ι → R),
  ‖∏ i ∈ t, (1 + f i) - 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1
-- Mathlib.RingTheory.IdealFilter.Topology
/-- Under `[F.IsUniform]`, `A` is a topological ring with the induced topology.  -/
WithIdealFilter.instIsTopologicalRing : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} [F.IsUniform], IsTopologicalRing (WithIdealFilter F)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.getKey! a l = Std.Internal.List.getKeyD a l default
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSub.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Sub β],
  MeasureTheory.SimpleFunc.instSub = { sub := fun f g => (MeasureTheory.SimpleFunc.map (fun x1 x2 => x1 - x2) f).seq g }
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepRet.eq_5 : ∀ (x : List ℕ) (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.fix f k) x =
    if x.headI = 0 then Turing.ToPartrec.stepRet k x.tail
    else Turing.ToPartrec.stepNormal f (Turing.ToPartrec.Cont.fix f k) x.tail
-- Mathlib.RingTheory.Adjoin.FGBaseChange
exists_fg_and_mem_baseChange : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (x : TensorProduct R A B), ∃ C, C.FG ∧ x ∈ Subalgebra.baseChange A C
-- Std.Async.System
Std.Async.System.OSInfo.mk.sizeOf_spec : ∀ (name release version machine : String),
  sizeOf { name := name, release := release, version := version, machine := machine } =
    1 + sizeOf name + sizeOf release + sizeOf version + sizeOf machine
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.Mem.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (a : α),
  aig.Mem a = (Std.Sat.AIG.Decl.atom a ∈ aig.decls)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- Given a property `P` of objects for `F : Pseudofunctor B Cat` and a morphism `f : X ⟶ Y`
in `B`, this is the functor `P.Obj X ⥤ P.Obj Y` that is induced by `F.map f`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.map : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      (P : F.ObjectProperty) →
        [P.IsClosedUnderMapObj] → {X Y : B} → (X ⟶ Y) → CategoryTheory.Functor (P.Obj X) (P.Obj Y)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.isIso_factorThruCoimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {P Q : C}
  (f : P ⟶ Q) [CategoryTheory.Epi f], CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruCoimage f)
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
PseudoMetricSpace.toIsCompletelPseudoMetrizableSpace : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [CompleteSpace X], TopologicalSpace.IsCompletelyPseudoMetrizableSpace X
-- Lean.Meta.Tactic.Grind.EMatch
/-- Checks whether `vars` satisfies the `grind_pattern` constraints attached at `thm`.
Example:
```
grind_pattern map_map => map g (map f xs) where
  f =/= some
  g =/= some
```
In the example above, a `map_map` instance should be added to the logical context only if
`f` and `g` are not definitionally equal to `some`

Remark: `proof` is used to extract the universe parameters in the proof.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.checkConstraints : Lean.Meta.Grind.EMatchTheorem → ℕ → Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.foldrMUnsafe.fold : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (α → β → m β) → Array α → USize → USize → β → m β
-- Init.Data.List.Nat.Range
List.getLast?_zipIdx : ∀ {α : Type u_1} {l : List α} {k : ℕ}, (l.zipIdx k).getLast? = Option.map (fun a => (a, k + l.length - 1)) l.getLast?
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_Iio_val : ∀ {n : ℕ} (i : Fin n), Fin.val ⁻¹' Set.Iio ↑i = Set.Iio i
-- Mathlib.Analysis.Real.Sqrt
Real.le_sqrt_self_iff : ∀ {x : ℝ}, x ≤ √x ↔ x ≤ 1
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.funLike : {M : Type u_4} → {N : Type u_5} → [inst : Zero M] → [inst_1 : Zero N] → FunLike (ZeroHom M N) M N
-- Mathlib.Data.List.Destutter
List.destutter'.congr_simp : ∀ {α : Type u_1} (R R_1 : α → α → Prop),
  R = R_1 →
    ∀ {inst : DecidableRel R} [inst_1 : DecidableRel R_1] (a a_1 : α),
      a = a_1 → ∀ (a_2 a_3 : List α), a_2 = a_3 → List.destutter' R a a_2 = List.destutter' R_1 a_1 a_3
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.instPowInt : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Pow (SpecialLinearGroup R V) ℤ
-- Mathlib.NumberTheory.RamificationInertia.Unramified
/-- For a prime `𝔓` of `S` lying over an unramified prime `𝔭` of `R`, the ramification index
`e(𝔓 ∣ 𝔭)` equals `1`.  -/
Algebra.IsUnramifiedIn.ramificationIdx_eq_one : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [Module.Finite ℤ R] [CharZero R] [Algebra.EssFiniteType R S] [Algebra.IsIntegral R S] {𝔭 : Ideal R},
  Algebra.IsUnramifiedIn S 𝔭 → ∀ {𝔓 : Ideal S} [𝔓.IsPrime], 𝔓.LiesOver 𝔭 → 𝔓.ramificationIdx R = 1
-- Init.PropLemmas
ite_then_decide_self : ∀ (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool), (if p then decide p else q) = (decide p || q)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexRange_apply : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (x : ↑(Set.range ⇑b)), b.reindexRange x = ↑x
-- Mathlib.Order.JordanHolder
/-- The equivalence relation on intervals generated by the relations `Iso (x, x ⊔ y) (x ⊓ y, y)` for
`IsMaximal x (x ⊔ y)`. This is the strongest possibly equivalence relation for which we can prove
the Jordan Hölder theorem. For any specific `JordanHolderLattice`, use `Iso.rel` to verify that
`Iso` implies the desired weaker notion (e.g., isomorphism of quotients).  -/
JordanHolderLattice.Iso : {X : Type u} → [inst : Lattice X] → [JordanHolderLattice X] → X × X → X × X → Prop
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
/-- **Alias** of the reverse direction of `MeasureTheory.memLp_piLp_iff`. -/
MeasureTheory.MemLp.of_eval_piLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p q : ENNReal} [inst : Fact (1 ≤ q)]
  {ι : Type u_2} [inst_1 : Fintype ι] {E : ι → Type u_3} [inst_2 : (i : ι) → NormedAddCommGroup (E i)]
  {f : X → PiLp q E}, (∀ (i : ι), MeasureTheory.MemLp (fun x => (f x).ofLp i) p μ) → MeasureTheory.MemLp f p μ
-- Init.Data.Vector.Count
Vector.count_eq_zero_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α} {xs : Vector α n}, a ∉ xs → Vector.count a xs = 0
-- Mathlib.Data.Set.Sups
HasInfs.mk : {α : Type u_4} → (α → α → α) → HasInfs α
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.renameFun_monomial : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : Semiring R]
  (x : σ →₀ ℕ) (r : R),
  MvPowerSeries.renameFun f ((MvPowerSeries.monomial x) r) = (MvPowerSeries.monomial (Finsupp.mapDomain f x)) r
-- Init.Data.UInt.Bitwise
UInt16.toUInt64_or : ∀ (a b : UInt16), (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
-- Lean.Meta.Hint
Lean.Meta.Hint.Suggestion.mk.injEq : ∀ (toTryThisSuggestion : Lean.Meta.Tactic.TryThis.Suggestion) (span? previewSpan? : Option Lean.Syntax)
  (diffGranularity : Lean.Meta.Hint.DiffGranularity) (toTryThisSuggestion_1 : Lean.Meta.Tactic.TryThis.Suggestion)
  (span?_1 previewSpan?_1 : Option Lean.Syntax) (diffGranularity_1 : Lean.Meta.Hint.DiffGranularity),
  ({ toTryThisSuggestion := toTryThisSuggestion, span? := span?, previewSpan? := previewSpan?,
        diffGranularity := diffGranularity } =
      { toTryThisSuggestion := toTryThisSuggestion_1, span? := span?_1, previewSpan? := previewSpan?_1,
        diffGranularity := diffGranularity_1 }) =
    (toTryThisSuggestion = toTryThisSuggestion_1 ∧
      span? = span?_1 ∧ previewSpan? = previewSpan?_1 ∧ diffGranularity = diffGranularity_1)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_iUnion_closure_eq_closure_iUnion : ∀ {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α),
  M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Generalized eigenvalues are actually just eigenvalues.  -/
Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ∞}, 0 < k → (f.HasUnifEigenvalue μ k ↔ f.HasUnifEigenvalue μ 1)
-- Mathlib.Order.Comparable
IncompRel.not_gt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], IncompRel (fun x1 x2 => x1 ≤ x2) a b → ¬b < a
-- Mathlib.Data.Matrix.Basic
AlgHom.mapMatrix_comp : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [inst : Fintype m]
  [inst_1 : DecidableEq m] [inst_2 : CommSemiring R] [inst_3 : Semiring α] [inst_4 : Semiring β] [inst_5 : Semiring γ]
  [inst_6 : Algebra R α] [inst_7 : Algebra R β] [inst_8 : Algebra R γ] (f : β →ₐ[R] γ) (g : α →ₐ[R] β),
  f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_iff_target_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e' : OpenPartialHomeomorph M' H'}
  {f : M → M'} {s : Set M} {x : M} {n : WithTop ℕ∞},
  e' ∈ IsManifold.maximalAtlas I' n M' →
    f x ∈ e'.source →
      (ContMDiffWithinAt I I' n f s x ↔
        ContinuousWithinAt f s x ∧ ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n (↑(e'.extend I') ∘ f) s x)
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- Variant of `MeromorphicOn.circleIntegrable_log_norm` for non-negative radii.
 -/
MeromorphicOn.circleIntegrable_log_norm_of_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c R) → 0 ≤ R → CircleIntegrable (fun x => Real.log ‖f x‖) c R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_alter_of_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} {f : Option β → Option β},
  cmp k k' = Ordering.eq → (k' ∈ Std.ExtDTreeMap.Const.alter t k f ↔ (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true)
-- Mathlib.Data.NNReal.Defs
NNReal.instInv : Inv NNReal
-- Mathlib.CategoryTheory.Triangulated.Rotate
/-- The counit isomorphism of the auto-equivalence of categories `triangleRotation C` of
`Triangle C` given by the rotation of triangles.  -/
CategoryTheory.Pretriangulated.invRotCompRot : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          (CategoryTheory.Pretriangulated.invRotate C).comp (CategoryTheory.Pretriangulated.rotate C) ≅
            CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.List.forIn'_eq_foldlM.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.yield b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_1 b
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- `range f` is invariant under `T` if and only if `f ∘L T ∘L f = T ∘L f`,
for idempotent `f`.  -/
ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f T : M →L[R] M},
  IsIdempotentElem f → ((↑f).range ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = T ∘SL f)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldCast.eq_1 : ∀ {n : ℕ} (α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldCast._auto_1✝ → Type u) {i j : ℕ} {hi : i ≤ n} (w : i = j)
  (x : α i hi), Nat.dfoldCast✝ α w x = w ▸ x
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.le : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} {J : Type w}
  {inst_1 : LinearOrder J} {inst_2 : SuccOrder J} {inst_3 : OrderBot J} {inst_4 : WellFoundedLT J}
  [self : W.IsStableUnderTransfiniteCompositionOfShape J], W.transfiniteCompositionsOfShape J ≤ W
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Finset V}
  (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V) (x : V),
  (finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq).repr x =
    lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) x)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.mul_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ) (f g : AdicCompletion.AdicCauchySequence I R),
  ↑(f * g) n = ↑f n * ↑g n
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.instLE : {X : Type u_1} → {R : Type u_2} → [inst : Zero R] → [inst_1 : Add R] → [inst_2 : LE R] → LE (PseudoMetric X R)