mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.Algebra.moduleAux_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] (a : A)
  (b : B) (m : M), (TensorProduct.Algebra.moduleAux (a ⊗ₜ[R] b)) m = a • b • m
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `lowerHemicontinuousOn_singleton_iff`. -/
ContinuousOn.lowerHemicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s → LowerHemicontinuousOn (fun x => {f x}) s
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.pbind.eq_1 : ∀ {m : Type w → Type w'} [inst : Monad m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α)
  (f : (a : α) → x.Property a → Std.Iterators.HetT m β),
  x.pbind f =
    { Property := fun b => ∃ a, ∃ (h : x.Property a), (f a h).Property b, small := ⋯,
      operation := do
        let a ← x.operation
        (fun b => Std.Internal.USquash.deflate ⟨↑b.inflate, ⋯⟩) <$> (f ↑a.inflate ⋯).operation }
-- Mathlib.Algebra.Order.Sub.Basic
tsub_right_inj : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → c ≤ a → (a - b = a - c ↔ b = c)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc : ∀ {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 j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (β : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f') (n : ℤ),
  autoParam (β = CategoryTheory.ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯)
      CategoryTheory.Abelian.SpectralObject.p_opcyclesMap._auto_1 →
    ∀ {Z : C} (h : X.opcycles f' g' n ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n)
          (CategoryTheory.CategoryStruct.comp (X.opcyclesMap f g f' g' α n) h) =
        CategoryTheory.CategoryStruct.comp ((X.H n).map β) (CategoryTheory.CategoryStruct.comp (X.pOpcycles f' g' n) h)
-- Mathlib.FieldTheory.Galois.Basic
/-- The intermediate field of fixed points fixed by a monoid action that commutes with the
`F`-action on `E`.  -/
FixedPoints.intermediateField : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (M : Type u_3) →
            [inst_3 : Monoid M] → [inst_4 : MulSemiringAction M E] → [SMulCommClass M F E] → IntermediateField F E
-- Init.Data.Int.DivMod.Lemmas
Int.mul_add_bmod_self_left : ∀ (a : ℕ) (b c : ℤ), (↑a * b + c).bmod a = c.bmod a
-- Init.Data.List.ToArray
List.findSome?_toArray : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α), Array.findSome? f l.toArray = List.findSome? f l
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.isSubDPIdeal_iSup : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {ι : Type u_3} {J : ι → Ideal A},
  (∀ (i : ι), hI.IsSubDPIdeal (J i)) → hI.IsSubDPIdeal (iSup J)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.equiv_iff_toList_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.toList = t₂.toList)
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply_finset' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Finset α}, MeasurableSet ↑s → MeasureTheory.Measure.count ↑s = ↑s.card
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.prod_le_pow_card : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M),
  (∀ x ∈ l, x ≤ n) → l.prod ≤ n ^ l.length
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_mul : ∀ {R : Type u_1} [inst : Semiring R] (f g : Polynomial R) {F G : ℕ},
  f.natDegree ≤ F →
    g.natDegree ≤ G → Polynomial.reflect (F + G) (f * g) = Polynomial.reflect F f * Polynomial.reflect G g
-- Init.Core
DoResultPR.return.inj : ∀ {α β σ : Type u} {a : β} {a_1 : σ} {a_2 : β} {a_3 : σ},
  DoResultPR.return a a_1 = DoResultPR.return a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
HasSum.mul_eq : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [T3Space α]
  [inst_2 : NonUnitalNonAssocSemiring α] [IsTopologicalSemiring α] {f : ι → α} {g : κ → α} {s t u : α},
  HasSum f s → HasSum g t → HasSum (fun x => f x.1 * g x.2) u → s * t = u
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfLeftIso_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.Limits.pullbackConeOfLeftIso f g).snd =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt
-- Mathlib.Data.List.OfFn
List.equivSigmaTuple_apply_fst : ∀ {α : Type u} (l : List α), (List.equivSigmaTuple l).fst = l.length
-- Batteries.Lean.Except
_private.Batteries.Lean.Except.0.Except.map.match_1.eq_2 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (v : α) (h_1 : (err : ε) → motive (Except.error err))
  (h_2 : (v : α) → motive (Except.ok v)),
  (match Except.ok v with
    | Except.error err => h_1 err
    | Except.ok v => h_2 v) =
    h_2 v
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.nonempty_iff : ∀ (X : Type u_3), Nonempty (FundamentalGroupoid X) ↔ Nonempty X
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The special case of the first simplicial identity  -/
SimplexCategory.δ_comp_δ_self : ∀ {n : ℕ} {i : Fin (n + 2)},
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ i.castSucc) =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ i.succ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, k ∉ t₂ → Std.DTreeMap.Const.getD (t₁ ∪ t₂) k fallback = Std.DTreeMap.Const.getD t₁ k fallback
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueMonoid_eq_closure : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B),
  f.valueMonoid = Submonoid.closure (Units.val ⁻¹' Set.range ⇑f)
-- Mathlib.Data.Num.Bitwise
PosNum.instHShiftRightNatNum : HShiftRight PosNum ℕ Num
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.sup_support_coeff_multisetProd_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B},
  degb 0 ≤ 0 →
    (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
      ∀ (m : Multiset (AddMonoidAlgebra R A)),
        m.prod.coeff.support.sup degb ≤ (Multiset.map (fun f => f.coeff.support.sup degb) m).sum
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The `PairingCore` structure induced by a pairing. The opposite construction
is `PairingCore.pairing`.  -/
SSet.Subcomplex.Pairing.pairingCore : {X : SSet} → {A : X.Subcomplex} → (P : A.Pairing) → [P.IsProper] → A.PairingCore
-- Mathlib.Data.Stream.Init
Stream'.take_append_of_le_length : ∀ {α : Type u} (n : ℕ) (x : List α) (a : Stream' α), n ≤ x.length → Stream'.take n (x ++ₛ a) = List.take n x
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def'_norm_cert : Int.Internal.Linear.Var →
  Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Lean.Meta.Basic
Lean.Meta.instInhabitedState : Inhabited Lean.Meta.State
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.mkOfAddEqZero.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : IsDedekindFiniteAddMonoid α] (a b : α) (hab : a + b = 0),
  AddUnits.mkOfAddEqZero a b hab = { val := a, neg := b, val_neg := hab, neg_val := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.keysArray_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keysArray = t₂.keysArray
-- Mathlib.Combinatorics.Configuration
/-- A type synonym.  -/
Configuration.Dual : Type u_1 → Type u_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_1.congr_eq_1 : ∀ {n : ℕ} (motive : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → Sort u_1)
  (x : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (h_1 : Unit → motive none)
  (h_2 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, true)))
  (h_3 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, false))),
  x = none →
    (match x with
      | none => h_1 ()
      | some (l, true) => h_2 l
      | some (l, false) => h_3 l) ≍
      h_1 ()
-- Mathlib.Combinatorics.Graph.Subgraph
/-- `H ≤s G` (`Graph.IsSpanningSubgraph`) is a subgraph of `G` with the same vertex set.  -/
Graph.IsSpanningSubgraph : {α : Type u_1} → {β : Type u_2} → Graph α β → Graph α β → Prop
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseEraNarrow : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Year.Era
-- Mathlib.NumberTheory.PrimeCounting
Nat.le_of_mem_primesLE : ∀ {p n : ℕ}, p ∈ n.primesLE → p ≤ n
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.one_div_pos_of_nat : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℕ}, 0 < 1 / (↑n + 1)
-- Mathlib.Logic.Nontrivial.Defs
not_subsingleton_iff_nontrivial : ∀ {α : Type u_1}, ¬Subsingleton α ↔ Nontrivial α
-- Mathlib.Analysis.Analytic.Basic
AnalyticOn.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E},
  AnalyticOn 𝕜 f t → s ⊆ t → AnalyticOn 𝕜 f s
-- Mathlib.Data.FunLike.Equiv
EquivLike.comp_bijective : ∀ {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [inst : EquivLike F β γ] (f : α → β) (e : F),
  Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f
-- Mathlib.NumberTheory.JacobiSum.Basic
gaussSum_pow_eq_prod_jacobiSum_aux : ∀ {F : Type u_1} {R : Type u_2} [inst : Fintype F] [inst_1 : Field F] [inst_2 : CommRing R] [IsDomain R]
  (χ : MulChar F R) (ψ : AddChar F R) {n : ℕ},
  0 < n → n < orderOf χ → gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Finset.Ico 1 n, jacobiSum χ (χ ^ j)
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.elabGrindConfig' : Lean.TSyntax `Lean.Parser.Tactic.optConfig → Bool → Lean.Elab.Tactic.TacticM Lean.Grind.Config
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isStrictlySupported_op_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c'), K.op.IsStrictlySupported e.op ↔ K.IsStrictlySupported e
-- Mathlib.Topology.Order.Category.AlexDisc
/-- Sends a topological space to its specialisation order.  -/
alexDiscEquivPreord : AlexDisc ≌ Preord
-- Mathlib.GroupTheory.Perm.Option
/-- Permutations of `Option α` are equivalent to fixing an
`Option α` and permuting the remaining with a `Perm α`.
The fixed `Option α` is swapped with `none`.  -/
Equiv.Perm.decomposeOption : {α : Type u_1} → [DecidableEq α] → Equiv.Perm (Option α) ≃ Option α × Equiv.Perm α
-- Mathlib.Data.String.Defs
/-- Pad `s : String` with repeated occurrences of `c : Char` on the right until it's of length `n`.
If `s` is initially larger than `n`, just return `s`.  -/
String.rightpad : ℕ → optParam Char ' ' → String → String
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- A complex polarization identity, with a linear map.  -/
inner_map_polarization : ∀ {V : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) (x y : V),
  inner ℂ (T y) x =
    (inner ℂ (T (x + y)) (x + y) - inner ℂ (T (x - y)) (x - y) +
          Complex.I * inner ℂ (T (x + Complex.I • y)) (x + Complex.I • y) -
        Complex.I * inner ℂ (T (x - Complex.I • y)) (x - Complex.I • y)) /
      4
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage.eq_1 : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X) (n : ℕ),
  Dynamics.dynEntourage T U n = ⋂ k, ⋂ (_ : k < n), (Prod.map T T)^[k] ⁻¹' U
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_swap_mul_eq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) (x : α),
  f (f x) ≠ x → (Equiv.swap x (f x) * f).support = f.support \ {x}
-- Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
CategoryTheory.Abelian.instIsMultiplicativeEpiWithInjectiveKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.Abelian.epiWithInjectiveKernel.IsMultiplicative
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instInhabited : {R : Type u} → [inst : NonAssocSemiring R] → Inhabited (Subsemiring R)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.toSSetFunctor_map : ∀ {X : SSet} {X_1 Y : X.Subcomplex} (h : X_1 ⟶ Y), SSet.Subcomplex.toSSetFunctor.map h = SSet.Subcomplex.homOfLE ⋯
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_neg_pos_pos_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ},
  ↑(3 • A).card ≤ K * ↑A.card → ↑(-A + A + A).card ≤ K ^ 2 * ↑A.card
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.mul_counit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : C) [inst_3 : CategoryTheory.BimonObj M] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom h)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchClone.isNatType : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCocone φ =
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) (-1)).obj (CochainComplex.mappingCone φ)
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restriction.sc'Iso_inv_τ₂ : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) {i' j' k' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k'),
  (HomologicalComplex.restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv.τ₂ = (K.restrictionXIso e hj').inv
-- Mathlib.Order.SymmDiff
bihimp_def : ∀ {α : Type u_2} [inst : Min α] [inst_1 : HImp α] (a b : α), bihimp a b = (b ⇨ a) ⊓ (a ⇨ b)
-- Init.Data.Nat.Basic
Nat.mul_pow : ∀ (a b n : ℕ), (a * b) ^ n = a ^ n * b ^ n
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two vector spaces are isomorphic if they have the same dimension.  -/
LinearEquiv.ofRankEq : {R : Type u} →
  (M M₁ : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [Module.Free R M] →
            [inst_4 : AddCommMonoid M₁] →
              [inst_5 : Module R M₁] →
                [Module.Free R M₁] → [StrongRankCondition R] → Module.rank R M = Module.rank R M₁ → M ≃ₗ[R] M₁
-- Mathlib.Data.List.Indexes
List.mapIdxMAux'.eq_2 : ∀ {m : Type v → Type w} [inst : Monad m] {α : Type u_7} (f : ℕ → α → m PUnit.{v + 1}) (x : ℕ) (a : α) (as : List α),
  List.mapIdxMAux' f x (a :: as) = f x a *> List.mapIdxMAux' f (x + 1) as
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- `NonUnitalAlgSemiHomClass F φ A B` asserts `F` is a type of bundled algebra homomorphisms
from `A` to `B` which are equivariant with respect to `φ`.  -/
NonUnitalAlgSemiHomClass : (F : Type u_1) →
  {R : outParam (Type u_2)} →
    {S : outParam (Type u_3)} →
      [inst : Monoid R] →
        [inst_1 : Monoid S] →
          outParam (R →* S) →
            (A : outParam (Type u_4)) →
              (B : outParam (Type u_5)) →
                [inst_2 : NonUnitalNonAssocSemiring A] →
                  [inst_3 : NonUnitalNonAssocSemiring B] →
                    [DistribMulAction R A] → [DistribMulAction S B] → [FunLike F A B] → Prop
-- Mathlib.Util.Notation3
/-- `notation3` argument.  -/
Mathlib.Notation3.notation3Item : Lean.ParserDescr
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.anyM.match_1.splitter : (motive : Bool → Sort u_1) → (__do_lift : Bool) → (Unit → motive true) → (Unit → motive false) → motive __do_lift
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {T : CategoryTheory.Monad C} → (A : T.Algebra) → Inhabited (A.Hom A)
-- Mathlib.Logic.Basic
ne_of_ne_of_eq : ∀ {α : Sort u_1} {a b c : α}, a ≠ b → b = c → a ≠ c
-- Mathlib.Order.Cover
/-- If `a < b` then there exist `a' > a` and `b' < b` such that `Set.Iio a'` is strictly to the left
of `Set.Ioi b'`.  -/
LT.lt.exists_disjoint_Iio_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDidChangeTextDocumentParams : Lean.Lsp.FileSource Lean.Lsp.DidChangeTextDocumentParams
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.postcomposeHomEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G) (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.IsLimit.postcomposeHomEquiv α c =
    CategoryTheory.Limits.IsLimit.ofConeEquiv (CategoryTheory.Limits.Cone.postcomposeEquivalence α)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.map_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  (E : CategoryTheory.PreZeroHypercover S), (CategoryTheory.PreZeroHypercover.map F E).I₀ = E.I₀
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instIsCentralScalar : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] {R : Type u_5}
  [inst_5 : Semiring R] [inst_6 : Module R A] [inst_7 : SMulCommClass 𝕜 R A] [inst_8 : ContinuousConstSMul R A]
  [inst_9 : IsScalarTower R A A] [inst_10 : SMulCommClass R A A] [inst_11 : Module Rᵐᵒᵖ A]
  [inst_12 : IsCentralScalar R A], IsCentralScalar R (DoubleCentralizer 𝕜 A)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mem_restrict_range : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] {r : β} {s : Set α}
  {f : MeasureTheory.SimpleFunc α β}, MeasurableSet s → (r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ Set.univ ∨ r ∈ ⇑f '' s)
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.support_killCompl : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f)
  {p : MvPolynomial τ R}, ((MvPolynomial.killCompl hf) p).support = p.support.preimage (Finsupp.mapDomain f) ⋯
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
/-- If `f` is absolutely continuous on `uIcc a b`, then `f'` is interval integrable on `a..b`.  -/
AbsolutelyContinuousOnInterval.intervalIntegrable_deriv : ∀ {f : ℝ → ℝ} {a b : ℝ}, AbsolutelyContinuousOnInterval f a b → IntervalIntegrable (deriv f) MeasureTheory.volume a b
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instContinuousMulAutFunctorFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  ContinuousMul (CategoryTheory.Aut F)
-- Lean.CompactedRegion
_private.Lean.CompactedRegion.0.Lean.CompactorSpec : NonemptyType
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.unitOfList_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  Std.ExtDHashMap.Const.unitOfList l = List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.apply_pure_cons_entails_l : ∀ {σs : List (Type u)} {Q : Std.Do.SPred σs} {φ : Prop} {σ : Type u} {s : σ}, (⌜φ⌝ ⊢ₛ Q) → ⌜φ⌝ s ⊢ₛ Q
-- Lean.Elab.Tactic.Simp
Lean.Meta.Simp.ConfigWithOptions.mk.inj : ∀ {config : Lean.Meta.Simp.Config} {userConfig : Lean.Options} {config_1 : Lean.Meta.Simp.Config}
  {userConfig_1 : Lean.Options},
  { config := config, userConfig := userConfig } = { config := config_1, userConfig := userConfig_1 } →
    config = config_1 ∧ userConfig = userConfig_1
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_eq_self : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] (A : Matrix m n α) (i : m), A.updateRow i (A i) = A
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertListConst_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)}
  {k fallback : α},
  (List.map Prod.fst toInsert).contains k = false →
    Std.Internal.List.getKeyD k (Std.Internal.List.insertListConst l toInsert) fallback =
      Std.Internal.List.getKeyD k l fallback
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.toFinsupp 0 = 0
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.pack_unpack_of_valid : ∀ {spec : Float.Model.Format} {b : BitVec spec.numBits},
  spec.Valid b →
    autoParam (2 ≤ spec.exponentBits) Float.Model.UnpackedFloat.pack_unpack_of_valid._auto_1 →
      Float.Model.UnpackedFloat.pack spec (Float.Model.UnpackedFloat.unpack spec b) = b
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.singleton_le_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {X : C} {P : CategoryTheory.ObjectProperty C},
  CategoryTheory.ObjectProperty.singleton X ≤ P ↔ P X
-- Mathlib.Logic.Equiv.Prod
optionProdEquiv_mk_none : ∀ {α : Type u_9} {β : Type u_10} (b : β), optionProdEquiv (none, b) = Sum.inl b
-- Mathlib.Order.Hom.Order
OrderHom.bot_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : OrderBot β],
  ⊥ = (OrderHom.const α) ⊥
-- Mathlib.Algebra.Order.UpperLower
Set.OrdConnected.vadd : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α} {a : α},
  s.OrdConnected → (a +ᵥ s).OrdConnected