mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- The underlying function `R → ℝ`.

Do NOT use directly. Use the coercion instead.  -/
StieltjesFunction.toFun : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → StieltjesFunction R → R → ℝ
-- Init.Data.Vector.Lex
_private.Init.Data.Vector.Lex.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- The maximal Følner filter with respect to some group `G` acting on a
measure space `X` is the pullback of `𝓝 0` along the map `s ↦ μ (g • s) / μ s`
on measurable sets of finite non-zero measure.  -/
maxFoelner : (G : Type u_1) →
  {X : Type u_2} →
    [inst : MeasurableSpace X] → MeasureTheory.Measure X → [inst : Group G] → [MulAction G X] → Filter (Set X)
-- Mathlib.RingTheory.KrullDimension.Zero
ringKrullDim.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R], ringKrullDim R = Order.krullDim (PrimeSpectrum R)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashSet α),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → m.getD a fallback = m_1.getD a_1 fallback_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km : α} (hc : t.contains k = true), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
someContDiffBumpBase.congr_simp : ∀ (E : Type u_3) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [hb : HasContDiffBump E],
  someContDiffBumpBase E = someContDiffBumpBase E
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
/-- See `add_tsub_le_assoc` for an inequality.  -/
add_tsub_assoc_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {b c : α} [AddLeftReflectLE α], c ≤ b → ∀ (a : α), a + b - c = a + (b - c)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsCircuit.contractElem_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α},
  M.IsCircuit C → C.Nontrivial → e ∈ C → (M.contract {e}).IsCircuit (C \ {e})
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.HaveTelescopeInfo.computeFixedUsed.updateArrayFromBackDeps : Array Bool → Std.HashSet ℕ → Array Bool
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyoneda.eq_1 : CommMonCat.coyoneda =
  {
    obj := fun M =>
      { obj := fun N => CommMonCat.of (↑(Opposite.unop M) →* ↑N),
        map := fun {X Y} f => CommMonCat.ofHom (MonoidHom.compHom (CommMonCat.Hom.hom f)), map_id := ⋯, map_comp := ⋯ },
    map := fun {X Y} f => { app := fun N => CommMonCat.ofHom (CommMonCat.Hom.hom f.unop).compHom', naturality := ⋯ },
    map_id := CommMonCat.coyoneda._proof_4, map_comp := @CommMonCat.coyoneda._proof_5 }
-- Lean.Meta.Tactic.Grind.Internalize
/-- If `e` is a `cast`-like term (e.g., `cast h a`), add `e ≍ a` to the to-do list.
It could be an E-matching theorem, but we want to ensure it is always applied since
we want to rely on the fact that `cast h a` and `a` are in the same equivalence class.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.pushCastHEqs : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Action.Monoidal
Action.forget_μ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X Y : Action V G),
  CategoryTheory.Functor.LaxMonoidal.μ (Action.forget V G) X Y =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((Action.forget V G).obj X) ((Action.forget V G).obj Y))
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_mul_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] (m₁ m₂ : M) (r₁ r₂ : R),
  AddMonoidAlgebra.single m₁ r₁ * AddMonoidAlgebra.single m₂ r₂ = AddMonoidAlgebra.single (m₁ + m₂) (r₁ * r₂)
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C),
  AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.inv.app X =
    AlgebraicTopology.DoldKan.Γ₂.map (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.inv.app X)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.equivMapOfInjective_invFun_coe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K : LieSubalgebra R L) (hf : Function.Injective ⇑f)
  (a : ↥(Submodule.map (↑f) K.toSubmodule)), ↑((LieSubalgebra.equivMapOfInjective f K hf).invFun a) = Classical.choose ⋯
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAlgebra : (S : Type u_1) →
  (R : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring S] →
        [inst_1 : CommSemiring R] →
          [inst_2 : NonUnitalSemiring A] →
            [inst_3 : Module R A] →
              [inst_4 : IsScalarTower R A A] →
                [inst_5 : SMulCommClass R A A] →
                  [inst_6 : Algebra S R] →
                    [inst_7 : DistribMulAction S A] → [IsScalarTower S R A] → Algebra S (Unitization R A)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.δ₀_concat : ∀ {X : SSet} {n : ℕ} (self : X.StrictSegalCore n) (x : X.obj (Opposite.op { len := 1 }))
  (s : X.obj (Opposite.op { len := n }))
  (h :
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
      (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) (self.concat x s h) = s
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.instOrderHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β], OrderHomClass (α →+o β) α β
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.rightUnitor_def : ∀ (R : Type u) [inst : CommRing R] (X : BialgCat R),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor X = (Bialgebra.TensorProduct.rid R R X.carrier).toBialgIso
-- Mathlib.Algebra.BigOperators.ModEq
Int.sum_modEq_ite : ∀ {α : Type u_1} {n : ℤ} {f : α → ℤ} [inst : DecidableEq α] {s : Finset α} {a : α},
  (∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]) → ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [ZMOD n]
-- Lean.Elab.BuiltinNotation
/-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))`  -/
Lean.Elab.Term.mkPairs : Array Lean.Term → Lean.MacroM Lean.Term
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestRevMatchAt_of_get : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.startPos},
  p ((pos.prev h).get ⋯) = true → String.Slice.Pattern.Model.IsLongestRevMatchAt p (pos.prev h) pos
-- Init.Data.SInt.Lemmas
Int8.toISize_mod : ∀ (a b : Int8), (a % b).toISize = a.toISize % b.toISize
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {w x y : C} (f : w ⟶ x) (g : x ⟶ y) (z : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.CategoryStruct.comp f g) z =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft g z)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_eq_C : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ {f : Polynomial R} {r : R}, (Polynomial.expand R p) f = Polynomial.C r ↔ f = Polynomial.C r
-- Mathlib.Data.Set.Lattice
Set.iInter_psigma : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : PSigma γ → Set β), ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.cokernelSequence_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.cokernelSequence f).X₂ = Y
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_rangeRestrict : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), f.rangeRestrict.ker = f.ker
-- Mathlib.Data.Fintype.Card
Fintype.card_subtype : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : Fintype { a // p a }] [inst_2 : DecidablePred p],
  Fintype.card { x // p x } = {x | p x}.card
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_add_projection_eq_self`. -/
Submodule.IsCompl.projection_add_projection_eq_self : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (p.projection q hpq) x + (q.projection p ⋯) x = x
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instCommMonoid.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : CommMonoid Y],
  LocallyConstant.instCommMonoid = Function.Injective.commMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Init.Data.String.PosRaw
String.Pos.Raw.le_trans : ∀ {a b c : String.Pos.Raw}, a ≤ b → b ≤ c → a ≤ c
-- Init.Data.Int.Lemmas
Int.ofNat_mul_negOfNat : ∀ (m n : ℕ), ↑m * Int.negOfNat n = Int.negOfNat (m * n)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_congr : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : SMulWithZero R S]
  [inst_3 : Monoid S] (f g : LaurentPolynomial R) (x y : Sˣ), f = g → x = y → f.smeval x = g.smeval y
-- Mathlib.Algebra.Algebra.Operations
/-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets
on either side).  -/
Submodule.span.ringHom : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → SetSemiring A →+* Submodule R A
-- Mathlib.Data.List.Basic
List.get_reverse' : ∀ {α : Type u} (l : List α) (n : Fin l.reverse.length) (hn' : l.length - 1 - ↑n < l.length),
  l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩
-- Init.Data.Int.Linear
Int.Internal.Linear.OrOver_cases_type : ℕ → (ℕ → Prop) → Prop
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_eq_top : ∀ {G : Type u_2} [inst : AddGroup G] {S : AddSubgroup G}, S.op = ⊤ ↔ S = ⊤
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.instFintypeSubtypeMemOfDecidablePred : {G : Type u_1} → [inst : AddGroup G] → (K : AddSubgroup G) → [DecidablePred fun x => x ∈ K] → [Fintype G] → Fintype ↥K
-- Mathlib.Order.SuccPred.Limit
IsMin.isSuccPrelimit : ∀ {α : Type u_1} {a : α} [inst : Preorder α], IsMin a → Order.IsSuccPrelimit a
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_zero : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (p : MvPolynomial σ R), (MvPolynomial.aeval 0) p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)
-- Std.Time.Date.Unit.Day
Std.Time.Day.Ordinal.instToStringOfYear : {leap : Bool} → ToString (Std.Time.Day.Ordinal.OfYear leap)
-- Init.Data.String.Iterate
String.Slice.ByteIterator.mk.inj : ∀ {s : String.Slice} {offset : String.Pos.Raw} {s_1 : String.Slice} {offset_1 : String.Pos.Raw},
  { s := s, offset := offset } = { s := s_1, offset := offset_1 } → s = s_1 ∧ offset = offset_1
-- Mathlib.Data.ENat.Lattice
ENat.biSup_add' : ∀ {ι : Sort u_2} {a : ℕ∞} {p : ι → Prop},
  (∃ i, p i) → ∀ (f : ι → ℕ∞), (⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a
-- Mathlib.RingTheory.Int.Basic
Int.instDecidablePredPrime : DecidablePred Prime
-- Mathlib.Logic.Unique
/-- Given an explicit `a : α` with `Subsingleton α`, we can construct
a `Unique α` instance. This is a def because the typeclass search cannot
arbitrarily invent the `a : α` term. Nevertheless, these instances are all
equivalent by `Unique.Subsingleton.unique`.

See note [reducible non-instances].  -/
uniqueOfSubsingleton : {α : Sort u_1} → [Subsingleton α] → α → Unique α
-- Init.Grind.Norm
Lean.Grind.eq_true_eq : ∀ (p : Prop), (p = True) = p
-- Mathlib.Data.Set.Restrict
Set.range_codRestrict : ∀ {α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s),
  Set.range (Set.codRestrict f s h) = Subtype.val ⁻¹' Set.range f
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Composition of two diffeomorphisms.  -/
Diffeomorph.trans : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {F : Type u_4} →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_5} →
                        [inst_7 : TopologicalSpace H] →
                          {H' : Type u_6} →
                            [inst_8 : TopologicalSpace H'] →
                              {G : Type u_7} →
                                [inst_9 : TopologicalSpace G] →
                                  {I : ModelWithCorners 𝕜 E H} →
                                    {I' : ModelWithCorners 𝕜 E' H'} →
                                      {J : ModelWithCorners 𝕜 F G} →
                                        {M : Type u_9} →
                                          [inst_10 : TopologicalSpace M] →
                                            [inst_11 : ChartedSpace H M] →
                                              {M' : Type u_10} →
                                                [inst_12 : TopologicalSpace M'] →
                                                  [inst_13 : ChartedSpace H' M'] →
                                                    {N : Type u_11} →
                                                      [inst_14 : TopologicalSpace N] →
                                                        [inst_15 : ChartedSpace G N] →
                                                          {n : WithTop ℕ∞} →
                                                            Diffeomorph I I' M M' n →
                                                              Diffeomorph I' J M' N n → Diffeomorph I J M N n
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.instMeasurableSMulNNReal : MeasurableSMul NNReal ENNReal
-- Mathlib.Probability.Independence.Process.Basic
/-- If `X` is a process independent from `Y` and for all `i`, `X' i` is almost everywhere equal
to `X i`, then `X'` is also independent from `Y`. This implies that independence results about
measurable processes should generally also hold
for processes whose marginals are only a.e.-measurable.  -/
ProbabilityTheory.Kernel.IndepFun.process_congr_right : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : Type u_6}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : MeasurableSpace 𝓨] {X X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  ProbabilityTheory.Kernel.IndepFun Y (fun ω i => X i ω) κ P →
    (∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i) → ProbabilityTheory.Kernel.IndepFun Y (fun ω i => X' i ω) κ P
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.Option.elim.match_1.eq_2 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (y : β) (x : α → β)
  (h_1 : (x : α) → (x_1 : β) → (f : α → β) → motive (some x) x_1 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match none, y, x with
    | some x, x_1, f => h_1 x x_1 f
    | none, y, x => h_2 y x) =
    h_2 y x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getElem_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {hk : k ∈ t₁} (h : t₁.Equiv t₂), t₁[k] = t₂[k]
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn_3.go : {motive_1 : Lean.Language.SnapshotTree → Sort u} →
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
    {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
      {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u} →
        {motive_5 : Task Lean.Language.SnapshotTree → Sort u} →
          (t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) →
            ((t : Lean.Language.SnapshotTree) → t.below → motive_1 t) →
              ((t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                  Lean.Language.SnapshotTree.below_1 t → motive_2 t) →
                ((t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                    Lean.Language.SnapshotTree.below_2 t → motive_3 t) →
                  ((t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) →
                      Lean.Language.SnapshotTree.below_3 t → motive_4 t) →
                    ((t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t) →
                      motive_4 t ×' Lean.Language.SnapshotTree.below_3 t
-- Mathlib.Algebra.Ring.Defs
/-- An associative but not-necessarily unital ring.  -/
NonUnitalRing : Type u_1 → Type u_1
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (toEquiv toEquiv_1 : α ≃ β)
  (e_toEquiv : toEquiv = toEquiv_1) (measurable_toFun : Measurable ⇑toEquiv)
  (measurable_invFun : Measurable ⇑toEquiv.symm),
  { toEquiv := toEquiv, measurable_toFun := measurable_toFun, measurable_invFun := measurable_invFun } =
    { toEquiv := toEquiv_1, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.Algebra.Group.Action.Defs
IsCentralScalar.unop_smul_eq_smul : ∀ {M : Type u_9} {α : Type u_10} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α),
  MulOpposite.unop m • a = m • a
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessResult.type : Lean.Meta.PreprocessResult✝ → Lean.Expr
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
FredholmDecomposition.mk : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            (X₀ X₁ : Submodule 𝕜 E) → Submodule.IsTopCompl X₁ X₀ → FiniteDimensional 𝕜 ↥X₀ → FredholmDecomposition 𝕜 E
-- Init.Tactics
/-- The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or
non-dependent hypotheses. It has many variants:
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.-
- If an `hᵢ` is a defined constant `f`, then `f` is unfolded. If `f` has equational lemmas associated
  with it (and is not a projection or a `reducible` definition), these are used to rewrite with `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the
  attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged
  with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If
  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis
  `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
  other hypotheses.
 -/
Lean.Parser.Tactic.simp : Lean.ParserDescr
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.CokernelData.π_lift : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] {pres₂ : Module.Presentation A M₂} {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (self : pres₂.CokernelData f g₁) (i : ι), pres₂.π (self.lift i) = f (g₁ i)
-- Init.Data.UInt.Bitwise
UInt64.toNat_shiftRight : ∀ (a b : UInt64), (a >>> b).toNat = a.toNat >>> (b.toNat % 64)
-- Mathlib.LinearAlgebra.Multilinear.DirectSum
/-- The linear equivalence between families indexed by `p : Π i : ι, κ i` of multilinear maps
on the `fun i ↦ M i (p i)` and the space of multilinear map on `fun i ↦ ⨁ j : κ i, M i j`.  -/
MultilinearMap.fromDirectSumEquiv : {R : Type u_1} →
  {ι : Type u_2} →
    {M' : Type u_3} →
      {κ : ι → Type u_4} →
        {M : (i : ι) → κ i → Type u_5} →
          [inst : CommSemiring R] →
            [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] →
              [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] →
                [inst_3 : AddCommMonoid M'] →
                  [inst_4 : Module R M'] →
                    [DecidableEq ι] →
                      [Finite ι] →
                        ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) M') ≃ₗ[R]
                          MultilinearMap R (fun i => DirectSum (κ i) fun j => M i j) M'
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnriched_comp_id : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₂],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedId V F₂))
        (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₂)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
-- Mathlib.Order.Concept
subset_lowerPolar_upperPolar : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α), s ⊆ lowerPolar r (upperPolar r s)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.uniformContinuous_ofLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → UniformSpace (β i)], UniformContinuous WithLp.ofLp
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)`. Construct a new tree with one key-value pair `k, v`.  -/
RBTree.RBMap.single : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → α → β → RBTree.RBMap α β cmp
-- Mathlib.Algebra.Order.Sub.WithTop
WithTop.sub_eq_top_iff : ∀ {α : Type u_1} [inst : Sub α] [inst_1 : Bot α] {a b : WithTop α}, a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
-- Mathlib.Order.Filter.Basic
Filter.set_eventuallyEq_iff_inf_principal : ∀ {α : Type u} {s t : Set α} {l : Filter α}, s =ᶠ[l] t ↔ l ⊓ Filter.principal s = l ⊓ Filter.principal t