mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_mul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : Mul β] [inst_2 : Mul γ] {g : β → γ},
  (∀ (x y : β), g (x * y) = g x * g y) →
    ∀ (f₁ f₂ : MeasureTheory.SimpleFunc α β),
      MeasureTheory.SimpleFunc.map g (f₁ * f₂) = MeasureTheory.SimpleFunc.map g f₁ * MeasureTheory.SimpleFunc.map g f₂
-- Mathlib.Order.WithBot
WithTop.coe_mono : ∀ {α : Type u_1} [inst : Preorder α], Monotone fun a => ↑a
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.freeMapIdIso_inv_app : ∀ (V : Type u_1) [inst : Quiver V] (X : CategoryTheory.Paths V),
  (CategoryTheory.Cat.freeMapIdIso V).inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
Submodule.FG.lTensor.directLimit.eq_1 : ∀ (R : Type u) (M : Type u_1) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq { Q // Q.FG }],
  Submodule.FG.lTensor.directLimit R M N =
    (TensorProduct.directLimitRight (fun x x_1 => Submodule.inclusion) M).symm.trans
      (LinearEquiv.lTensor M (Submodule.FG.directLimit R N))
-- Init.Data.SInt.Lemmas
Int8.toInt32_toInt64 : ∀ (n : Int8), n.toInt64.toInt32 = n.toInt32
-- Std.Http.Data.Version
Std.Http.instBEqVersion.beq : Std.Http.Version → Std.Http.Version → Bool
-- Init.Core
Eq.to_iff : ∀ {a b : Prop}, a = b → (a ↔ b)
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.restrictScalars_traceDual : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] {I : Submodule B L},
  Submodule.restrictScalars A (Submodule.traceDual A K I) =
    (Algebra.traceForm K L).dualSubmodule (Submodule.restrictScalars A I)
-- Init.Data.Array.Find
Array.findSome?_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : γ → Option α} {f : β → γ} {xs : Array β},
  Array.findSome? p (Array.map f xs) = Array.findSome? (p ∘ f) xs
-- Init.Data.SInt.Bitwise
Int16.and_assoc : ∀ (a b c : Int16), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.indicator_biUnion_apply : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset ι) (t : ι → Set κ) {f : κ → β},
  (↑s).PairwiseDisjoint t → ∀ (x : κ), (⋃ i ∈ s, t i).indicator f x = ∑ i ∈ s, (t i).indicator f x
-- Mathlib.Algebra.Ring.CentroidHom
/-- Copy of a `CentroidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
CentroidHom.copy : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → (f : CentroidHom α) → (f' : α → α) → f' = ⇑f → CentroidHom α
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkLineEq.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integralCLM'.congr_simp : ∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [inst : NormedAddCommGroup E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E]
  [inst_4 : IsBoundedSMul 𝕜 E] [inst_5 : SMulCommClass ℝ 𝕜 E] [inst_6 : CompleteSpace E],
  MeasureTheory.L1.integralCLM' 𝕜 = MeasureTheory.L1.integralCLM' 𝕜
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapFunctor_obj : ∀ (T : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T),
  (CategoryTheory.Over.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Over X)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_eq_of_lt_invVeblen₁ : ∀ {o x : Ordinal.{u}}, o < x.invVeblen₁ → Ordinal.veblen o x = x
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsMulLeftInvariant],
  μ'.haarScalarFactor μ = if ¬LocallyCompactSpace G then 1 else ⋯.choose
-- Mathlib.Tactic.Linter.TextBased
/-- Core logic of a text based linter: given a collection of lines,
return an array of all style errors with (1-based!) line numbers. If possible,
also return the collection of all lines, changed as needed to fix the linter errors.
(Such automatic fixes are only possible for some kinds of `StyleError`s.)
 -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.TextbasedLinter : Type
-- Init.Data.SInt.Lemmas
ISize.pow_succ : ∀ (x : ISize) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivAt.add` -/
HasDerivAt.fun_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (fun i => f i + g i) (f' + g') x
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaEquiv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ}
  {P Q : CategoryTheory.Functor C (Type w)} (α : CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X ⟶ P) (β : P ⟶ Q),
  CategoryTheory.shrinkCoyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.ConcreteCategory.hom (β.app (Opposite.unop X))) (CategoryTheory.shrinkCoyonedaEquiv α)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extInv.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (φ φ_1 : c.pt ≅ c'.pt) (e_φ : φ = φ_1)
  (w : ∀ (j : J), c.ι.app j = CategoryTheory.CategoryStruct.comp (c'.ι.app j) φ.inv),
  CategoryTheory.Limits.Cocone.extInv φ w = CategoryTheory.Limits.Cocone.extInv φ_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.mapGL_inj : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [FaithfulSMul R S] (g g' : Matrix.SpecialLinearGroup n R),
  (Matrix.SpecialLinearGroup.mapGL S) g = (Matrix.SpecialLinearGroup.mapGL S) g' ↔ g = g'
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- If `f : M → N` is a monoid hom, then `MonoidAlgebra.mapDomain f` is a bialgebra hom between
their monoid algebras.  -/
MonoidAlgebra.mapDomainBialgHom : (R : Type u_1) →
  {M : Type u_8} →
    {N : Type u_9} →
      [inst : CommSemiring R] →
        [inst_1 : Monoid M] → [inst_2 : Monoid N] → (M →* N) → MonoidAlgebra R M →ₐc[R] MonoidAlgebra R N
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.unsat_of_cons_none_unsat : ∀ {n : ℕ} (clauses : List (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))),
  Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
      (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray (none :: clauses).toArray) →
    Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
      (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray clauses.toArray)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_apply : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i) (x : PiTensorProduct 𝕜 fun i => E i),
  (PiTensorProduct.mapL f) x = (PiTensorProduct.map fun i => ↑(f i)) x
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond.eq_4 : ∀ (n k : ℕ), n.succ.stirlingSecond k.succ = (k + 1) * n.stirlingSecond (k + 1) + n.stirlingSecond k
-- Init.Notation
/-- `(min+1)` (we can only write `min+1` after `Meta.lean`)  -/
precMin1 : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
Homeomorph.toMeasurableEquiv.congr_simp : ∀ {γ : Type u_3} {γ₂ : Type u_4} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ]
  [inst_3 : TopologicalSpace γ₂] [inst_4 : MeasurableSpace γ₂] [inst_5 : BorelSpace γ₂] (h h_1 : γ ≃ₜ γ₂),
  h = h_1 → h.toMeasurableEquiv = h_1.toMeasurableEquiv
-- Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Set.mem_list_prod : ∀ {α : Type u_1} [inst : Monoid α] {l : List (Set α)} {a : α},
  a ∈ l.prod ↔ ∃ l', (List.map (fun x => ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = l
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.extend_apply_self : ∀ {B : Type u_2} (F : Type u_3) {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] [inst_3 : (x : B) → Zero (E x)]
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_5 : FiberBundle F E] {x : B} (v : E x),
  FiberBundle.extend F v x = v
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffAddMonoidHom_apply : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (p : MvPolynomial σ R),
  (MvPolynomial.coeffAddMonoidHom m) p = MvPolynomial.coeff m p
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.refl_source : ∀ {α : Type u_1}, (PartialEquiv.refl α).source = Set.univ
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.mapA.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.ofAlgEquiv_toGenerators : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T),
  (P.ofAlgEquiv e).toGenerators = P.ofAlgEquiv e
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- The antitone order embedding of closed subsets of `Spec R` into ideals of `R`.  -/
PrimeSpectrum.closedsEmbedding : (R : Type u_1) → [inst : CommSemiring R] → (TopologicalSpace.Closeds (PrimeSpectrum R))ᵒᵈ ↪o Ideal R
-- Init.Data.SInt.Lemmas
Int16.ofInt_bitVecToInt : ∀ (n : BitVec 16), Int16.ofInt n.toInt = Int16.ofBitVec n
-- Std.Data.ExtHashMap.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `getElem_insertIfNew`.  -/
Std.ExtHashMap.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β}, a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.instInhabited : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → Inhabited (CategoryTheory.GrothendieckTopology C)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.coe_toPartialEquiv_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e.symm = ↑e.symm
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts : ∀ {α : Type u_1} {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : μ.Regular], MeasureTheory.IsFiniteMeasureOnCompacts μ
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.matched_of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos endPos' : s.Pos} {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidRevSearchFrom pat startPos l →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos' →
      endPos = endPos' →
        String.Slice.Pattern.Model.IsValidRevSearchFrom pat endPos'
          (String.Slice.Pattern.SearchStep.matched startPos endPos :: l)
-- Lean.Elab.InfoTree.Types
Lean.Elab.UserWidgetInfo.mk.inj : ∀ {toWidgetInstance : Lean.Widget.WidgetInstance} {stx : Lean.Syntax} {toWidgetInstance_1 : Lean.Widget.WidgetInstance}
  {stx_1 : Lean.Syntax},
  { toWidgetInstance := toWidgetInstance, stx := stx } = { toWidgetInstance := toWidgetInstance_1, stx := stx_1 } →
    toWidgetInstance = toWidgetInstance_1 ∧ stx = stx_1
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.ext : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I),
  (∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x) → hI = hI'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.beq_iff_equiv : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : BEq β]
  [LawfulBEq α] [LawfulBEq β], Std.DHashMap.Const.beq m₁ m₂ = true ↔ m₁.Equiv m₂
-- Mathlib.Algebra.Algebra.Hom
/-- In a tower, the canonical map from the middle element to the top element is an
algebra homomorphism over the bottom element.  -/
IsScalarTower.toAlgHom : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R S] → [inst_4 : Algebra S A] → [inst_5 : Algebra R A] → [IsScalarTower R S A] → S →ₐ[R] A
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_apply : ∀ {σ : Type u_1} {R : Type u_4} [inst : AddCommMonoid R] (d : σ →₀ R), Finsupp.degree d = ∑ i ∈ d.support, d i
-- Mathlib.Order.Shrink
instPredOrderShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [inst_1 : Preorder α] → [PredOrder α] → PredOrder (Shrink.{u, u_1} α)
-- Mathlib.NumberTheory.Real.Irrational
exists_rat_of_not_irrational : ∀ {x : ℝ}, ¬Irrational x → ∃ q, x = ↑q
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom
      (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f U.ι) h
-- Mathlib.Analysis.Normed.Group.Continuity
continuous_norm' : ∀ {E : Type u_4} [inst : SeminormedGroup E], Continuous fun a => ‖a‖
-- Mathlib.Algebra.Group.Hom.Defs
/-- If `f` is a monoid homomorphism then `f (a * b) = f a * f b`.  -/
MonoidHom.map_mul : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N) (a b : M), f (a * b) = f a * f b
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- If a group `G` acts faithfully on `α`, then
it acts faithfully on `powersetCard α n` provided `1 ≤ n < ENat.card α`.  -/
Set.powersetCard.faithfulSMul : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  1 ≤ n → ↑n < ENat.card α → ∀ [FaithfulSMul G α], FaithfulSMul G ↑(Set.powersetCard α n)
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.instIsSemitopologicalSemiring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [IsSemitopologicalSemiring A] (s : NonUnitalStarSubalgebra R A),
  IsSemitopologicalSemiring ↥s
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_mul_right₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Mul β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) → ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.IndepFun (f i) (f j * f k) μ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_smul : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g : E → 𝕜},
  Function.HasTemperateGrowth g → ∀ (c : 𝕜), SchwartzMap.smulLeftCLM F (c • g) = c • SchwartzMap.smulLeftCLM F g
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
/-- Right tensoring a module with a quotient of the ring is the same as
quotienting that module by the corresponding submodule.  -/
TensorProduct.tensorQuotEquivQuotSMul : {R : Type u_1} →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (I : Ideal R) → TensorProduct R M (R ⧸ I) ≃ₗ[R] M ⧸ I • ⊤
-- Lean.Meta.ProdN
/-- Given a product `(e₁, e₂)` of type `t₁ × t₂`, return `(e₁, t₁, e₂, t₂)`.  -/
Lean.Meta.getProdFields : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.IsFinitePresentation.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  {q : M.QuasicoherentData},
  autoParam (∀ (i : q.I), (q.presentation i).IsFinite)
      SheafOfModules.QuasicoherentData.IsFinitePresentation.isFinite_presentation._autoParam →
    q.IsFinitePresentation
-- Mathlib.Algebra.Group.Nat.Range
Finset.disjoint_range_addRightEmbedding : ∀ (a : ℕ) (s : Finset ℕ), Disjoint (Finset.range a) (Finset.map (addRightEmbedding a) s)
-- Mathlib.Algebra.Ring.Defs
neg_mul : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * b = -(a * b)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_apply : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (a : MvPolynomial (Option S₁) R),
  (MvPolynomial.optionEquivLeft R S₁) a =
    (MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (MvPolynomial.X s)) a
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- A more convenient way of obtaining a unique gluing of sections for a sheaf.
 -/
TopCat.Sheaf.existsUnique_gluing : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  (F : TopCat.Sheaf C X) {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X)
  (sf : (i : ι) → CategoryTheory.ToType (F.obj.obj (Opposite.op (U i)))),
  TopCat.Presheaf.IsCompatible F.obj U sf → ∃! s, TopCat.Presheaf.IsGluing F.obj U sf s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] {a : α}, Std.Internal.List.getKey! a [] = default
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.p_fromOpcycles_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) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C}
  (h_1 : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n)
      (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n) h_1) =
    CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) h_1
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a monoid homomorphism `f : N → M` and a congruence relation `c` on `M`, the congruence
relation induced on `N` by `f` equals the kernel of `c`'s quotient homomorphism composed with
`f`.  -/
Con.comap_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {c : Con M} {f : N →* M},
  Con.comap ⇑f ⋯ c = Con.ker (c.mk'.comp f)
-- Mathlib.Data.List.Intervals
List.Ico.eq_1 : ∀ (n m : ℕ), List.Ico n m = List.range' n (m - n)
-- Mathlib.CategoryTheory.Category.Cat
/-- Composition in the category of categories equals functor composition.  -/
CategoryTheory.Cat.comp_eq_comp : ∀ {X Y Z : CategoryTheory.Cat} (F : X ⟶ Y) (G : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp F G).toFunctor = F.toFunctor.comp G.toFunctor
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {v : β}, (t.insertIfNew k v).getKey? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.getKey? a
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexiveCoforkEquivCofork_functor_obj_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  (G : CategoryTheory.Limits.ReflexiveCofork F),
  ((CategoryTheory.Limits.reflexiveCoforkEquivCofork F).functor.obj G).π = G.π
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mem_add : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P) (x : P), x ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.eq_of_not_ssubset`.

---

Set notation form of `LE.le.eq_of_not_lt` -/
HasSubset.Subset.eq_of_not_ssubset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → ¬a ⊂ b → a = b
-- Mathlib.Topology.GDelta.Basic
/-- A nowhere dense set is meagre.  -/
IsNowhereDense.isMeagre : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsNowhereDense s → IsMeagre s
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.ofNat_ctorIdx : ∀ (x : Turing.PartrecToTM2.K'), Turing.PartrecToTM2.K'.ofNat x.ctorIdx = x
-- Mathlib.Analysis.BoundedVariation
eVariation_mul_le : ∀ {α : Type u_2} [inst : LinearOrder α] {f g : α → ℝ} {C D : ENNReal} {s : Set α},
  (∀ x ∈ s, ‖f x‖ₑ ≤ C) → (∀ x ∈ s, ‖g x‖ₑ ≤ D) → eVariationOn (f * g) s ≤ C * eVariationOn g s + D * eVariationOn f s
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalState.exprs : Lean.Meta.Grind.GoalState → Lean.PArray Lean.Expr
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.congr : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f g : X → ε} {μ : MeasureTheory.Measure X},
  MeasureTheory.LocallyIntegrable f μ → f =ᵐ[μ] g → MeasureTheory.LocallyIntegrable g μ
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_add : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Add α] (M N : Matrix (m × o) (n × o) α),
  (M + N).blockDiag = M.blockDiag + N.blockDiag
-- Lean.Meta.Tactic.Grind.CheckResult
/-- Updated basis, simplified equations.  -/
Lean.Meta.Grind.CheckResult.progress : Lean.Meta.Grind.CheckResult
-- Mathlib.Algebra.RingQuot
RingQuot.eqvGen_rel_eq : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop), Relation.EqvGen (RingQuot.Rel r) = RingConGen.Rel r
-- Mathlib.Data.Set.FiniteExhaustion
/-- Every set in a `FiniteExhaustion` is finite.  -/
Set.FiniteExhaustion.finite' : ∀ {α : Type u_1} {s : Set α} (self : s.FiniteExhaustion) (n : ℕ), Finite ↑(self.toFun n)