mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
DerivedCategory.singleFunctorIsoCompQ.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ),
  DerivedCategory.singleFunctorIsoCompQ C n = CategoryTheory.Iso.refl (DerivedCategory.singleFunctor C n)
-- Mathlib.Topology.Sheaves.CommRingCat
/-- Unfold `restrictOpen` in the category of commutative rings (with the correct carrier type).

Although unification hints help with applying `TopCat.Presheaf.restrictOpenCommRingCat`,
so it can be safely de-specialized, this lemma needs to be kept to ensure rewrites go right.
 -/
TopCat.Presheaf.restrictOpenCommRingCat_apply : ∀ {X : TopCat} {F : TopCat.Presheaf CommRingCat X} {V : TopologicalSpace.Opens ↑X} (f : ↑(F.obj (Opposite.op V)))
  (U : TopologicalSpace.Opens ↑X) (e : autoParam (U ≤ V) TopCat.Presheaf.restrictOpenCommRingCat_apply._auto_1),
  TopCat.Presheaf.restrictOpen f U e = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE e).op)) f
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.Transcendental.ringHom_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B] [inst_9 : RingHomClass FAB A B]
  (f : FRS) (g : FAB) [H : Algebra.Transcendental R A],
  Function.Surjective ⇑f →
    Function.Injective ⇑g → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → Algebra.Transcendental S B
-- Mathlib.Combinatorics.Digraph.Orientation
Digraph.toSimpleGraphStrict_mono : ∀ {V : Type u_1}, Monotone Digraph.toSimpleGraphStrict
-- Mathlib.Topology.Instances.CantorSet
preCantorSet_zero : preCantorSet 0 = Set.Icc 0 1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore_dim : ∀ {m : ℕ} (k : Fin (m + 1)) (n : ℕ) (s : SSet.prodStdSimplex.pairingCore.Type₁ k n),
  (SSet.prodStdSimplex.pairingCore k n).dim s = s.d
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The L-function of an even function vanishes at negative even integers.  -/
ZMod.LFunction_neg_two_mul_nat_add_one : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ}, Function.Even Φ → ∀ (n : ℕ), ZMod.LFunction Φ (-(2 * (↑n + 1))) = 0
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.wittPolyProd_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (WittVector.wittPolyProd p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.Algebra.Order.Field.Pointwise
LinearOrderedField.smul_Ioi : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a r : K},
  0 < r → r • Set.Ioi a = Set.Ioi (r * a)
-- Mathlib.Algebra.Star.Unitary
Unitary.mem_iff : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1
-- Mathlib.Algebra.Group.Support
Function.support_nsmul : ∀ {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] (f : α → M) (n : ℕ),
  (Function.support fun x => n • f x) ⊆ Function.support f
-- Lean.Declaration
Lean.Declaration.axiomDecl : Lean.AxiomVal → Lean.Declaration
-- Lean.Parser.Do
/-- `do← s` (or ASCII `do<- s`) hands `s` to the enclosing wrapper as a body
whose control-flow effects (`return`, `break`, `continue`, `mut`-variable
reassignment) target the surrounding `do` block, not the body's local monad.

The syntax is reminiscent of a nested action `(← s)`, but unlike a nested
action, `s` is not run eagerly in the `do` block context before the wrapping
function is called. The wrapping function decides when to run `s`, and code
is inserted to forward `s`'s effects to the outer `do` block.

Only valid as the last argument of a function application that itself appears
as a statement of an outer `do` block, optionally wrapped in `fun` binders.
Examples:
* `f a₁ … aₙ (do← s)`
* `f a₁ … aₙ (fun b₁ … bₖ => do← s)`
 -/
Lean.Parser.Term.doForward : Lean.Parser.Parser
-- Mathlib.Data.PNat.Basic
instIsOrderedCancelMonoidPNat : IsOrderedCancelMonoid ℕ+
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toList_toArray : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toArray.toList = it.toList
-- Mathlib.Order.Filter.Finite
Finset.eventuallyLE_iInter : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f g : ι → Set α},
  (∀ i ∈ s, f i ≤ᶠ[l] g i) → ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {a k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).get? a =
        if h : compare k a = Ordering.eq then some (cast ⋯ v) else t.get? a
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.ord_aleph : ∀ (o : Ordinal.{u_1}), (Cardinal.aleph o).ord = Ordinal.omega o
-- Mathlib.CategoryTheory.Sigma.Basic
/-- A function `J → I` induces a functor `Σ j, C (g j) ⥤ Σ i, C i`.  -/
CategoryTheory.Sigma.map : {I : Type w₁} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₂} → (g : J → I) → CategoryTheory.Functor ((j : J) × C (g j)) ((i : I) × C i)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_lt_add_right : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [inst_1 : LT α] [AddRightStrictMono α], z ≠ ⊤ → x < y → x + z < y + z
-- Mathlib.Algebra.Ring.Subring.Defs
/-- The natural ring hom from a subring of ring `R` to `R`.  -/
SubringClass.subtype : {R : Type u} →
  {S : Type v} → [inst : NonAssocRing R] → [inst_1 : SetLike S R] → [hSR : SubringClass S R] → (s : S) → ↥s →+* R
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.range_eq_empty_of_isEmpty : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_5} [hα : IsEmpty α] (f : MeasureTheory.SimpleFunc α β),
  f.range = ∅
-- Mathlib.Algebra.Group.PUnit
PUnit.instZero_mathlib.eq_1 : PUnit.instZero_mathlib = { zero := PUnit.unit }
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instSMulCoeOfSMulMemClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} {G : Type u_4} [inst_1 : (i : ι) → SMul G (R i)] [inst_2 : ∀ (i : ι), SMulMemClass (S i) G (R i)],
  RestrictedProduct.instSMulCoeOfSMulMemClass R = { smul := fun g x => ⟨fun i => g • x i, ⋯⟩ }
-- Mathlib.Topology.Bornology.Basic
Bornology.comap_cobounded_le_iff : ∀ {α : Type u_2} {β : Type u_3} {x : Bornology α} [inst : Bornology β] {f : α → β},
  Filter.comap f (Bornology.cobounded β) ≤ Bornology.cobounded α ↔
    ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalTermOccurrences : Lean.Elab.ConfigEval.EvalTerm Lean.Meta.Occurrences
-- Mathlib.MeasureTheory.Integral.Layercake
MeasureTheory.countable_meas_le_ne_meas_lt : ∀ {α : Type u_1} {R : Type u_2} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_1 : LinearOrder R]
  (g : α → R), {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}.Countable
-- Mathlib.CategoryTheory.Action.Basic
Action.functorCategoryEquivalence_inverse : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G],
  (Action.functorCategoryEquivalence V G).inverse = Action.FunctorCategoryEquivalence.inverse
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.rename.sizeOf_spec : ∀ (oldName : Lean.Name) (oldStx : Lean.Syntax) (newName : Lean.Name) (newStx : Lean.Syntax),
  sizeOf (Simps.ProjectionRule.rename oldName oldStx newName newStx) =
    1 + sizeOf oldName + sizeOf oldStx + sizeOf newName + sizeOf newStx
-- Init.Data.Option.Basic
/-- Checks whether an optional value is both present and equal to some other value.

Given `x? : Option α` and `y : α`, `x?.isEqSome y` is equivalent to `x? == some y`. It is more
efficient because it avoids an allocation.
 -/
Option.isEqSome : {α : Type u_1} → [BEq α] → Option α → α → Bool
-- Mathlib.RingTheory.Localization.Away.Basic
Localization.awayMap_awayMap_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (f : R →+* S) (a b : R),
  Function.Surjective ⇑(Localization.awayMap f (a * b)) →
    Function.Surjective ⇑(Localization.awayMap (Localization.awayMap f a) ((algebraMap R (Localization.Away a)) b))
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_succ_comp_X_sub_one : ∀ (R : Type u) [inst : Ring R] (n : ℕ),
  (descPochhammer R (n + 1)).comp (Polynomial.X - 1) =
    descPochhammer R (n + 1) - (↑n + 1) • (descPochhammer R n).comp (Polynomial.X - 1)
-- Mathlib.Topology.Algebra.Localization
instTopologicalSpaceLocalization : {R : Type u_1} → [inst : CommRing R] → [TopologicalSpace R] → {M : Submonoid R} → TopologicalSpace (Localization M)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- `SubringClass S R` states that `S` is a type of subsets `s ⊆ R` that
are both a multiplicative submonoid and an additive subgroup.  -/
SubringClass : (S : Type u_1) → (R : outParam (Type u)) → [NonAssocRing R] → [SetLike S R] → Prop
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_take_succ : ∀ {M : Type u_4} [inst : Monoid M] (L : List M) (i : ℕ) (p : i < L.length),
  (List.take (i + 1) L).prod = (List.take i L).prod * L[i]
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.toAddSubmonoid_le : ∀ {G : Type u_1} [inst : AddGroup G] {p q : AddSubgroup G}, p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.inclusion_comp_decomposedTo : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] (j : CategoryTheory.ConnectedComponents J),
  (CategoryTheory.inclusion j).comp (CategoryTheory.decomposedTo J) = j.ι
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_vadd : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VAdd α β] (s : ι → Set α) (t : Set β),
  (⋃ i, s i) +ᵥ t = ⋃ i, s i +ᵥ t
-- Mathlib.CategoryTheory.Functor.Basic
/-- Notation for the identity functor on a category.  -/
CategoryTheory.«term𝟭» : Lean.ParserDescr
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.powers_of_not_orderTop_pos : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R},
  ¬0 < x.orderTop → HahnSeries.SummableFamily.powers x = HahnSeries.SummableFamily.single 0 1
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsEquipartition.card_interedges_sparsePairs_le : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [inst_4 : DecidableRel G.Adj]
  {ε : 𝕜},
  P.IsEquipartition →
    0 ≤ ε →
      ↑((P.sparsePairs G ε).biUnion fun x =>
              match x with
              | (U, V) => G.interedges U V).card ≤
        4 * ε * ↑A.card ^ 2
-- Mathlib.RepresentationTheory.Invariants
Rep.invariantsAdjunction_homEquiv_apply_hom : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G] {X : ModuleCat k} {Y : Rep.{u_1, u, v} k G}
  (f : (Rep.trivialFunctor k G).obj X ⟶ Y),
  ModuleCat.Hom.hom (((Rep.invariantsAdjunction k G).homEquiv X Y) f) =
    LinearMap.codRestrict Y.ρ.invariants (Rep.Hom.hom f).toLinearMap ⋯
-- Mathlib.Logic.Relation
Relation.ReflTransGen.cases_head : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α},
  Relation.ReflTransGen r a b → a = b ∨ ∃ c, r a c ∧ Relation.ReflTransGen r c b
-- Batteries.Data.Char.AsciiCasing
Char.not_isLower_of_isUpper : ∀ {c : Char}, c.isUpper = true → ¬c.isLower = true
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {k : α} {f : β → β} (h : m.WF)
  {hc : k ∈ Std.DHashMap.Raw.Const.modify m k f},
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.modify m k f) k hc = f (Std.DHashMap.Raw.Const.get m k ⋯)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_map_equiv : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [inst_2 : MeasurableSpace β] (e : α ≃ᵐ β) {f : β → ε} {μ : MeasureTheory.Measure α}
  {s : Set β},
  MeasureTheory.IntegrableOn f s (MeasureTheory.Measure.map (⇑e) μ) ↔ MeasureTheory.IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' s) μ
-- Mathlib.Analysis.Normed.Affine.MazurUlam
IsometryEquiv.coe_toRealAffineIsometryEquiv : ∀ {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : MetricSpace PE] [inst_3 : NormedAddTorsor E PE] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F]
  [inst_6 : MetricSpace PF] [inst_7 : NormedAddTorsor F PF] (f : PE ≃ᵢ PF),
  f.toRealAffineIsometryEquiv.toIsometryEquiv = f
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- For `X` a simplicial set, `IsStrictSegal X` asserts the mere existence of
an inverse to `spine X n` for all `n : ℕ`.  -/
SSet.IsStrictSegal : SSet → Prop
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
  [T2Space M] [ContinuousSub M] {v : MeasureTheory.VectorMeasure α M} {s : ℕ → Set α},
  Antitone s → (∀ (i : ℕ), MeasurableSet (s i)) → Filter.Tendsto (fun n => v (s n)) Filter.atTop (nhds (v (⋂ n, s n)))
-- Lean.Elab.Do.Basic
/-- Given a list of mut vars `vars` and an FVar `tupleVar` binding a tuple, bind the mut vars to the
fields of the tuple and call `k` in the resulting local context.
 -/
Lean.Elab.Do.bindMutVarsFromTuple : List Lean.Name → Lean.FVarId → Lean.Elab.Do.DoElabM Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.range_map_eq_span_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (f : M →ₗ[R] P)
  (g : N →ₗ[R] Q), (TensorProduct.map f g).range = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNat.mk : ∀ {α : Type u} [inst : AddMonoidWithOne α] {a : α} {n : ℕ}, a = ↑n → Mathlib.Meta.NormNum.IsNat a n
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
Module.End.eigenspace_aeval_polynomial_degree_1 : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (f : Module.End K V)
  (q : Polynomial K), q.degree = 1 → f.eigenspace (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker ((Polynomial.aeval f) q)
-- Mathlib.SetTheory.Cardinal.ENat
/-- The coercion `Cardinal.ofENat` as a bundled homomorphism.  -/
Cardinal.ofENatHom : ℕ∞ →+*o Cardinal.{u_1}
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.ae_pi_le_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.ae (MeasureTheory.Measure.pi μ) ≤ Filter.pi fun i => MeasureTheory.ae (μ i)
-- Mathlib.Analysis.Calculus.Deriv.Inv
DifferentiableWithinAt.fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 d s x → d x ≠ 0 → DifferentiableWithinAt 𝕜 (fun x => c x / d x) s x
-- Init.Prelude
/-- Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `UInt8.ofNat 5 = 5`
* `UInt8.ofNat 255 = 255`
* `UInt8.ofNat 256 = 0`
* `UInt8.ofNat 259 = 3`
* `UInt8.ofNat 32770 = 2`
 -/
UInt8.ofNat : ℕ → UInt8
-- Mathlib.MeasureTheory.Integral.CompactlySupported
/-- Integral as a positive linear functional on `C_c(X, ℝ)`.  -/
CompactlySupportedContinuousMap.integralPositiveLinearMap : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [inst_1 : MeasurableSpace X] →
      [OpensMeasurableSpace X] →
        (μ : MeasureTheory.Measure X) →
          [MeasureTheory.IsFiniteMeasureOnCompacts μ] → CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ
-- Lean.DocString.Syntax
/-- A quotation, which contains a sequence of blocks that are at least as indented as the `>`.
 -/
Lean.Doc.Syntax.blockquote : Lean.ParserDescr
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_mul_sqrt_lt_succ' : ∀ (n : ℕ), n.sqrt ^ 2 < n + 1
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.equivFinsuppOfBasisRight_symm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq κ]
  (𝒞 : Module.Basis κ R N),
  ↑(TensorProduct.equivFinsuppOfBasisRight 𝒞).symm = (Finsupp.lsum R) fun i => (TensorProduct.mk R M N).flip (𝒞 i)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- If `f` and `g` are two maps `P → P'` between presentations,
their difference induces a map `P.CotangentSpace →ₗ[S] P'.Cotangent` that makes two maps
between the cotangent complexes homotopic.
 -/
Algebra.Extension.Hom.sub : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u'} →
              {S' : Type v'} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            [inst_8 : Algebra R S'] →
                              [IsScalarTower R R' S'] →
                                [IsScalarTower R S S'] → P.Hom P' → P.Hom P' → P.CotangentSpace →ₗ[S] P'.Cotangent
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- When a function has a limit at infinity, and its derivative is nonpositive, then the derivative
is automatically integrable on `(a, +∞)`. Version assuming differentiability
on `(a, +∞)` and continuity at `a⁺`.  -/
MeasureTheory.integrableOn_Ioi_deriv_of_nonpos : ∀ {g g' : ℝ → ℝ} {a l : ℝ},
  ContinuousWithinAt g (Set.Ici a) a →
    (∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Ioi a, g' x ≤ 0) →
        Filter.Tendsto g Filter.atTop (nhds l) → MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
-- Mathlib.GroupTheory.IsSubnormal
_private.Mathlib.GroupTheory.IsSubnormal.0.Subgroup.IsSubnormal.isSubnormal_iff.match_1_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ) (n : ℕ),
  x = n.succ →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_2 n
-- Mathlib.RingTheory.Frobenius
IsArithFrobAt.mem_stabilizer : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {G : Type u_3}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] {Q : Ideal S} {σ : G} [Q.IsPrime],
  IsArithFrobAt R σ Q → σ ∈ MulAction.stabilizer G Q
-- Mathlib.Tactic.Tauto
Mathlib.Tactic.Tauto.Config.noConfusionType : Sort v✝ → Mathlib.Tactic.Tauto.Config → Mathlib.Tactic.Tauto.Config → Sort v✝
-- Lean.Meta.IndPredBelow
/-- Map from proofs `h : ∀ x y z, ...` to pairs of `belowIndName` and a proof of
`h' : ∀ x y z, belowIndName ... (h x y z)`. These are used to find match rewriting candidates.
 -/
Lean.Meta.IndPredBelow.RecursionContext.belows : Lean.Meta.IndPredBelow.RecursionContext → Lean.FVarIdMap (Lean.Name × Lean.Expr)
-- Mathlib.Order.CompleteLattice.Basic
sInf_range : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] {f : ι → α}, sInf (Set.range f) = iInf f
-- Mathlib.Analysis.Matrix.Normed
/-- Normed space instance (using the Frobenius norm) for matrices over a normed space.  Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.frobeniusNormedSpace : {R : Type u_1} →
  {m : Type u_3} →
    {n : Type u_4} →
      {α : Type u_5} →
        [inst : Fintype m] →
          [inst_1 : Fintype n] →
            [inst_2 : NormedField R] →
              [inst_3 : SeminormedAddCommGroup α] → [NormedSpace R α] → NormedSpace R (Matrix m n α)
-- Lean.Data.PPContext
Lean.PPContext.currNamespace : Lean.PPContext → Lean.Name
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
/-- The product `r * x`, `r : ℚ`, `r ≠ 0`, is a Liouville number with exponent `p` if and only if
`x` satisfies the same condition.  -/
LiouvilleWith.rat_mul_iff : ∀ {p x : ℝ} {r : ℚ}, r ≠ 0 → (LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Addition of ordinal notations (correct only for normal input)  -/
ONote.add : ONote → ONote → ONote
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
Filter.EventuallyEq.mlieBracketWithin_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x},
  V₁ =ᶠ[nhdsWithin x s] V →
    W₁ =ᶠ[nhdsWithin x s] W →
      VectorField.mlieBracketWithin I V₁ W₁ s =ᶠ[nhdsWithin x s] VectorField.mlieBracketWithin I V W s
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induce_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {s : Set V} {u v : ↑s}, (SimpleGraph.induce s G).Adj u v ↔ G.Adj ↑u ↑v
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Subalgebra.isSimpleOrder_of_finrank : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E],
  Module.finrank F E = 2 → IsSimpleOrder (Subalgebra F E)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_fun_smul : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (c : ℝ) (f : X → E),
  ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_le_of_le_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν d : MeasureTheory.Measure α}, μ ≤ d + ν → μ - ν ≤ d
-- Lean.Syntax
/-- Compare the `SyntaxNodeKind`s in `pattern` to those of the `Syntax`
elements in `stack`. Return `false` if `stack` is shorter than `pattern`.  -/
Lean.Syntax.Stack.matches : Lean.Syntax.Stack → List (Option Lean.SyntaxNodeKind) → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂)[k]? = t₁[k]?
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The natural group hom from a subgroup of group `G` to `G`.  -/
SubgroupClass.subtype : {G : Type u_1} →
  [inst : Group G] → {S : Type u_4} → (H : S) → [inst_1 : SetLike S G] → [inst_2 : SubgroupClass S G] → ↥H →* G
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.ofFn.go.match_1.eq_1 : ∀ {n : ℕ} (motive : (x : ℕ) → x ≤ n → Sort u_1) (i : ℕ) (h : i + 1 ≤ n)
  (h_1 : (i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h) (h_2 : (x : 0 ≤ n) → motive 0 x),
  (match i.succ, h with
    | i.succ, h => h_1 i h
    | 0, x => h_2 x) =
    h_1 i h