mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.pointwise_smul_le_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : Group G] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G A]
  {S T : AddSubgroup A} {a : G}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Init.Control.Except
/-- Returns the value of a computation, forgetting whether it was an exception or a success.

This corresponds to early return.
 -/
ExceptT.runCatch : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → ExceptT α m α → m α
-- Mathlib.SetTheory.Cardinal.Order
WellOrderingRel.isWellOrder : ∀ {α : Type u}, IsWellOrder α WellOrderingRel
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.rightUnitor_inv_apply : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [inst_5 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  (X : CategoryTheory.GradedObject I C) (i : I),
  (CategoryTheory.GradedObject.Monoidal.rightUnitor X).inv i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X i)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X i) CategoryTheory.GradedObject.Monoidal.tensorUnit₀.inv)
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj X CategoryTheory.GradedObject.Monoidal.tensorUnit i 0 i ⋯))
-- Mathlib.Algebra.Group.Defs
SubtractionMonoid.neg_neg : ∀ {G : Type u} [self : SubtractionMonoid G] (x : G), - -x = x
-- Lean.Util.ParamMinimizer
/-- Restores parameter `i` after an unsuccessful removal
Sets bit `i` back to `true`.
 -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.restore : {m : Type → Type} → ℕ → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Unit
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.containsThenInsert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α} {b : β},
  t.WF → (t.containsThenInsert a b).2.WF
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalEquiv.toLinearEquiv : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst_1 : CommRing k] →
        [inst_2 : CharP k p] →
          [inst_3 : PerfectRing k p] →
            {V : Type u_2} →
              [inst_4 : AddCommGroup V] →
                [inst_5 : WittVector.Isocrystal p k V] →
                  {V₂ : Type u_3} →
                    [inst_6 : AddCommGroup V₂] →
                      [inst_7 : WittVector.Isocrystal p k V₂] →
                        WittVector.IsocrystalEquiv p k V V₂ → V ≃ₗ[FractionRing (WittVector p k)] V₂
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.resolventTransform_dirac : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜} [MeasurableSingletonClass 𝕜] [CompleteSpace A] (x : 𝕜) (a : A),
  MeasureTheory.resolventTransform (MeasureTheory.Measure.dirac x) a = resolvent a x
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
MeasureTheory.Measure.addHaarMeasure.congr_simp : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ K₀_1 : TopologicalSpace.PositiveCompacts G),
  K₀ = K₀_1 → MeasureTheory.Measure.addHaarMeasure K₀ = MeasureTheory.Measure.addHaarMeasure K₀_1
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_union : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq α] (s₁ s₂ : Multiset α),
  (s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.rightHom_comp_inl : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G), S.rightHom.comp S.inl = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.nonsingularPointEquiv_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R},
  W'.nonsingularPointEquiv WeierstrassCurve.Affine.Point.zero = none
-- Mathlib.Analysis.Normed.Field.Basic
/-- A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.  -/
NormedField : Type u_5 → Type u_5
-- Mathlib.Analysis.Calculus.FDeriv.Star
differentiableAt_star_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} [TrivialStar 𝕜],
  DifferentiableAt 𝕜 (fun y => star (f y)) x ↔ DifferentiableAt 𝕜 f x
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.inv_hom_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} (e : A ≅ B) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.δ_eq_iff : ∀ {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d) (i : Fin (d + 2)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) (y.cast ⋯).simplex =
      (x.cast hd).simplex ↔
    i = hxy.index hd
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- If `F` is an empty diagram,
then a cocone over `F` is colimiting iff the cocone point is initial.  -/
CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        [IsEmpty J] →
          {F : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cocone F) →
              CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsInitial c.pt
-- Init.Data.Option.Lemmas
Option.or_eq_orElse : ∀ {α : Type u_1} {o o' : Option α}, o.or o' = o.orElse fun x => o'
-- Lean.DocString.Parser
/-- A linebreak that isn't a block break (that is, there's non-space content on the next line)
 -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.linebreak : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.GroupTheory.GroupAction.ConjAct
/-- Reinterpret `g : G` as an element of `ConjAct G`.  -/
ConjAct.toConjAct : {G : Type u_3} → [inst : DivInvMonoid G] → G ≃* ConjAct G
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_add : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : ContinuousAdd M₂]
  (f g : M₁ →SL[σ₁₂] M₂), ↑(f + g) = ↑f + ↑g
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_zpow_coe_angle : ∀ (x : ℂ) (n : ℤ), ↑(x ^ n).arg = n • ↑x.arg
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a^2 | b)` is `1` when `a` and `b` are coprime.  -/
jacobiSym.sq_one' : ∀ {a : ℤ} {b : ℕ}, a.gcd ↑b = 1 → jacobiSym (a ^ 2) b = 1
-- Mathlib.Topology.Basic
isOpen_const : ∀ {X : Type u} [inst : TopologicalSpace X] {p : Prop}, IsOpen {_x | p}
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constModify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] (k : α) (f : β → β),
  m₁.Equiv m₂ → (Std.DHashMap.Const.modify m₁ k f).Equiv (Std.DHashMap.Const.modify m₂ k f)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_2 : ∀ {C : Type u} (X Y Z : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z) =
    id
      (CategoryTheory.Discrete.natTrans fun x =>
        CategoryTheory.CategoryStruct.id
          ((CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
                  Z).normalizeObj'.obj
            x))
-- Mathlib.Analysis.LocallyConvex.Montel
/-- If `E` is a Montel space, then the strong topology on `E →L[𝕜] F` coincides with the topology
of compact convergence.

We realize this equality in terms of a continuous linear equivalence between the type synonyms.  -/
ContinuousLinearEquiv.toCompactConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          (E : Type u_3) →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [IsTopologicalAddGroup E] →
                      [ContinuousSMul 𝕜₁ E] →
                        [inst_7 : AddCommGroup F] →
                          [inst_8 : Module 𝕜₂ F] →
                            [inst_9 : TopologicalSpace F] →
                              [inst_10 : IsTopologicalAddGroup F] →
                                [inst_11 : ContinuousSMul 𝕜₂ F] →
                                  [T1Space E] → [MontelSpace 𝕜₁ E] → (E →SL[σ] F) ≃L[𝕜₂] CompactConvergenceCLM σ E F
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.zero_divMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (s : σ →₀ ℕ), MvPolynomial.divMonomial 0 s = 0
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Mathlib.Data.Fin.Parity
Fin.even_iff_mod_of_even : ∀ {n : ℕ} {k : Fin n}, Even n → (Even k ↔ ↑k % 2 = 0)
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.instFiniteIdOfSearchStep : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] {pat : ρ}
  [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] {s : String.Slice} [Std.Iterators.Finite (σ s) Id],
  Std.Iterators.Finite (String.Slice.SplitInclusiveIterator pat s) Id
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpoly_sub_diagonal_degree_lt : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  (M.charpoly - ∏ i, (Polynomial.X - Polynomial.C (M i i))).degree < ↑(Fintype.card n - 1)
-- Mathlib.GroupTheory.Sylow
Sylow.characteristic_of_normal : ∀ {G : Type u} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  (↑P).Normal → (↑P).Characteristic
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.instInhabitedSimprocDeclExtState : Inhabited Lean.Meta.Simp.SimprocDeclExtState
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.bot_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], ⊥ = 0
-- Std.Time.Zoned
/-- Converts a `PlainDate` to a `Timestamp` using the `TimeZone`.
 -/
Std.Time.PlainDate.toTimestampWithZone : Std.Time.PlainDate → Std.Time.TimeZone → Std.Time.Timestamp
-- Mathlib.Data.Set.Image
Set.range_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (g : α → β) (f : ι → α), Set.range (g ∘ f) = g '' Set.range f
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.mapOfMeasurable.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ κ_1 : ProbabilityTheory.Kernel α β),
  κ = κ_1 → ∀ (f f_1 : β → γ) (e_f : f = f_1) (hf : Measurable f), κ.mapOfMeasurable f hf = κ_1.mapOfMeasurable f_1 ⋯
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_pow : ∀ {M : Type u_10} {F : Type u_11} [inst : Monoid M] [inst_1 : FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ)
  (x : M) (k : ℕ), (⇑f)^[n] (x ^ k) = (⇑f)^[n] x ^ k
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_triangle4_left : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x₁ y₁ x₂ y₂ : α), dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- **Alias** of the forward direction of `Matroid.Indep.isRkFinite_iff_finite`. -/
Matroid.Indep.finite_of_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → M.IsRkFinite I → I.Finite
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitAddMonoid : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [CategoryTheory.IsFiltered J] → AddMonoid (AddMonCat.FilteredColimits.M F)
-- Mathlib.Topology.UnitInterval
iccHomeoI_apply_coe : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : IsTopologicalRing 𝕜] (a b : 𝕜) (h : a < b) (x : ↑(Set.Icc a b)),
  ↑((iccHomeoI a b h) x) = (↑x - a) / (b - a)
-- Lean.Declaration
Lean.instInhabitedAxiomVal : Inhabited Lean.AxiomVal
-- Mathlib.Combinatorics.Configuration
Configuration.sum_lineCount_eq_sum_pointCount : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst_1 : Fintype P] [inst_2 : Fintype L],
  ∑ p, Configuration.lineCount L p = ∑ l, Configuration.pointCount P l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} [inst_1 : Inhabited (β k)],
  t.WF → (Std.DTreeMap.Internal.Impl.filter! f t).get! k = (Option.filter (f k) (t.get? k)).get!
-- Mathlib.Logic.Equiv.Set
Equiv.image_symm_image : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set β), ⇑e '' ⇑e.symm '' s = s
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ici_toDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α),
  Finset.Ici (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Iic a)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.step_flatMapM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [inst_2 : LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)}
  {it₁ : Std.IterM m β},
  (Std.IterM.flatMapM f it₁).step = do
    let __do_lift ← it₁.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it₁' b, h⟩ => do
        let fx ← MonadAttach.attach (f b)
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfterM f it₁' (some ↑fx)) ⋯))
      | ⟨Std.IterStep.skip it₁', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfterM f it₁' none) ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.mk : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    {u : E →L[𝕜] F} →
                      (decDom : FredholmDecomposition 𝕜 E) →
                        (decCodom : FredholmDecomposition 𝕜 F) →
                          (equiv : ↥decDom.X₁ ≃L[𝕜] ↥decCodom.X₁) →
                            u = decCodom.X₁.subtypeL ∘SL ↑equiv ∘SL decDom.proj → u.FredholmPackage
-- Mathlib.Data.ENNReal.Basic
Set.OrdConnected.preimage_coe_nnreal_ennreal : ∀ {u : Set ENNReal}, u.OrdConnected → (ENNReal.ofNNReal ⁻¹' u).OrdConnected
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.insert.eq_def : ∀ (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.insert k v p =
    match p with
    | Lean.Grind.Linarith.Poly.nil => Lean.Grind.Linarith.Poly.add k v Lean.Grind.Linarith.Poly.nil
    | Lean.Grind.Linarith.Poly.add k' v' p =>
      bif Nat.blt v' v then Lean.Grind.Linarith.Poly.add k v (Lean.Grind.Linarith.Poly.add k' v' p)
      else
        bif Nat.beq v v' then if (k.add k' == 0) = true then p else Lean.Grind.Linarith.Poly.add (k.add k') v' p
        else Lean.Grind.Linarith.Poly.add k' v' (Lean.Grind.Linarith.Poly.insert k v p)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (S : Set (Set α)) (t : Set β), ⋃₀ S +ᵥ t = ⋃ s ∈ S, s +ᵥ t
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.empty_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ∅ ∩ s = ∅
-- Mathlib.Algebra.Group.Action.Units
AddUnits.vaddCommClass_right : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} [inst : AddMonoid N] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddCommClass M N α], VAddCommClass M (AddUnits N) α
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.trans_inverse : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (e : CategoryTheory.IsoCat C D) (f : CategoryTheory.IsoCat D E), (e.trans f).inverse = f.inverse.comp e.inverse
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G H : CategoryTheory.Functor C (Type (max w v u)))
  (a : G ⟶ F.functorHom H) (X : C),
  ((CategoryTheory.FunctorToTypes.functorHomEquiv F G H) a).app X =
    TypeCat.ofHom fun x =>
      match x with
      | (x, y) =>
        (CategoryTheory.ConcreteCategory.hom
            (((CategoryTheory.ConcreteCategory.hom (a.app X)) y).app X (CategoryTheory.CategoryStruct.id X)))
          x
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.instOne : {G : Type u_1} → [inst : Add G] → {a : G} → One (AddConstMap G G a a)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.LeftLift.IsKan.fac_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.LeftLift f g) {Z : c ⟶ a}
  (h : CategoryTheory.CategoryStruct.comp s.lift f ⟶ Z),
  CategoryTheory.CategoryStruct.comp t.unit
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (H.desc s) f) h) =
    CategoryTheory.CategoryStruct.comp s.unit h
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_filter_not_contains_map_fst_eq_length_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    (∀ (a : α), Std.Internal.List.containsKey a l₁ = true → Std.Internal.List.containsKey a l₂ = false) →
      (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁).length = l₁.length
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.congr_fun : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e e' : M ≃ₛₗ[σ] M₂},
  e = e' → ∀ (x : M), e x = e' x
-- Mathlib.Algebra.Algebra.Tower
Submodule.smul_mem_span_smul' : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [IsScalarTower R S A] {s : Set S},
  Submodule.span R s = ⊤ →
    ∀ {t : Set A} {k : S} {x : A}, x ∈ Submodule.span R (s • t) → k • x ∈ Submodule.span R (s • t)
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- `Dilation.ratio` as a monoid homomorphism.  -/
DilationEquiv.ratioHom : {X : Type u_1} → [inst : PseudoEMetricSpace X] → (X ≃ᵈ X) →* NNReal
-- Mathlib.Order.Monotone.Monovary
Antivary.comp_monotone_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Antivary f g → Monotone f' → Antivary (f' ∘ f) g
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.specParser : Std.Internal.Parsec.String.Parser Std.Time.FormatString
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.right_mem_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ∈ Set.uIoc a b ↔ a < b
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.comap_cobounded_le : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → Filter.comap f (Bornology.cobounded β) ≤ Bornology.cobounded α
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tprod_pi_single : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : DecidableEq β] (b : β)
  (a : α), ∏' (b' : β), Pi.mulSingle b a b' = a
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
/-- The entropy of an entourage `U`, defined as the exponential rate of growth of the size
of the smallest `(U, n)`-refined cover of `F`. Takes values in the space of extended real numbers
`[-∞, +∞]`. This first version uses a `limsup`, and is chosen as the default definition.  -/
Dynamics.coverEntropyEntourage : {X : Type u_1} → (X → X) → Set X → SetRel X X → EReal
-- Mathlib.Topology.Separation.Basic
Homeomorph.t0Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T0Space X] (h : X ≃ₜ Y),
  T0Space Y
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalBitVec : {n : ℕ} → Lean.Meta.ReduceEval (BitVec n)
-- Lean.Declaration
Lean.instInhabitedConstantVal : Inhabited Lean.ConstantVal
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.CC'₀.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (g : ↑(Profinite.NobelingProof.C' C ho)),
  Profinite.NobelingProof.CC'₀ C ho g = ⟨↑g, ⋯⟩
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.auxEquiv_comm : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (x : GradedTensorProduct R 𝒜 ℬ),
  (GradedTensorProduct.auxEquiv R ℬ 𝒜) ((GradedTensorProduct.comm 𝒜 ℬ) x) =
    (TensorProduct.gradedComm R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) x)
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- An induction principle for `Projectivization`. Use as `induction v`.  -/
Projectivization.ind : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {P : Projectivization K V → Prop},
  (∀ (v : V) (h : v ≠ 0), P (Projectivization.mk K v h)) → ∀ (p : Projectivization K V), P p
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore.eq_1 : ∀ (base x : ℕ) (x_1 : List Char), base.toDigitsCore 0 x x_1 = x_1
-- Init.Data.UInt.Bitwise
UInt32.zero_xor : ∀ {a : UInt32}, 0 ^^^ a = a
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.finite_iff : ∀ {α : Type u_1} (M : Matroid α), M.Finite ↔ M.E.Finite
-- Mathlib.GroupTheory.OrderOfElement
mem_zmultiples_nsmul_iff : ∀ {G : Type u_1} [inst : AddGroup G] {g : G} {k : ℕ}, g ∈ AddSubgroup.zmultiples (k • g) ↔ k.gcd (addOrderOf g) = 1
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.genLt.formatter : Lean.PrettyPrinter.Formatter