mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α)
  (k : Equiv.Perm ↑(Function.fixedPoints ⇑g)) (v : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)),
  Equiv.Perm.sign ((Equiv.Perm.OnCycleFactors.kerParam g) (k, v)) = Equiv.Perm.sign k * ∏ c, Equiv.Perm.sign ↑(v c)
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_dite_eq' : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} [inst_2 : DecidableEq ι]
  (i : ι) (f : (j : ι) → j = i → M),
  (s.expect fun j => if h : j = i then f j h else 0) = if i ∈ s then (↑s.card)⁻¹ • f i ⋯ else 0
-- Mathlib.Algebra.Module.Presentation.Basic
/-- The module that is presented by generators and relations given by `relations : Relations A`.
This is the quotient of the free `A`-module on `relations.G` by the submodule generated by
the given relations.  -/
Module.Relations.Quotient : {A : Type u} → [inst : Ring A] → Module.Relations A → Type (max u w₀)
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_ofReal_mul : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ) (z : K), RCLike.im (↑r * z) = r * RCLike.im z
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Algebra.IsAlgebraic.trdeg_le_cardinalMk : ∀ (R : Type u_1) {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : Set A)
  [NoZeroDivisors A] [alg : Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A], Algebra.trdeg R A ≤ Cardinal.mk ↑s
-- Init.Notation
/-- The standardized "medium" priority `mid = 500`. This is lower than `default`, and higher than `low`.
 -/
prioMid : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.isClosedEmbedding_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsClosedEmbedding)
-- Mathlib.NumberTheory.Bernoulli
/-- **von Staudt-Clausen theorem:** For any natural number $k$, the sum
$$B_{2k} + \sum_{p - 1 \mid 2k} \frac{1}{p}$$ is an integer.
 -/
Bernoulli.vonStaudt_clausen : ∀ (k : ℕ),
  bernoulli (2 * k) + ∑ p ∈ Finset.range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p ∈ Set.range Int.cast
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceCodeActionParams : Lean.Lsp.FileSource Lean.Lsp.CodeActionParams
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.subtype_eq_univ : ∀ {α : Type u_1} {s : Finset α} {p : α → Prop} [inst : DecidablePred p] [inst_1 : Fintype { a // p a }],
  Finset.subtype p s = Finset.univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_if_push : ∀ {m n : ℕ}, (m...n).toArray = if m < n then (m...n - 1).toArray.push (n - 1) else #[]
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.serverNotInitialized.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.serverNotInitialized = 1
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α →CO β) (f' : α → β)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Init.Data.Vector.Algebra
Vector.instNoNatZeroDivisors : ∀ {α : Type u_1} {n : ℕ} [inst : Lean.Grind.NatModule α] [Lean.Grind.NoNatZeroDivisors α],
  Lean.Grind.NoNatZeroDivisors (Vector α n)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlg_comp : ∀ {A : Type u_3} (B : Type u_4) (C : Type u_5) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] [inst_5 : Algebra B C] [IsScalarTower A B C] (p : Polynomial A),
  (Polynomial.mapAlg A C) p = (Polynomial.mapAlg B C) ((Polynomial.mapAlg A B) p)
-- Lean.Parser.Command
/-- Skip input until the next whitespace character (used for error recovery for certain tokens)  -/
_private.Lean.Parser.Command.0.Lean.Parser.Command.skipUntilWs : Lean.Parser.Parser
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressParams.mk.injEq : ∀ (textDocument : Lean.Lsp.VersionedTextDocumentIdentifier) (processing : Array Lean.Lsp.LeanFileProgressProcessingInfo)
  (textDocument_1 : Lean.Lsp.VersionedTextDocumentIdentifier)
  (processing_1 : Array Lean.Lsp.LeanFileProgressProcessingInfo),
  ({ textDocument := textDocument, processing := processing } =
      { textDocument := textDocument_1, processing := processing_1 }) =
    (textDocument = textDocument_1 ∧ processing = processing_1)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
/-- The portion of `SzemerediRegularity.chunk` which is contained in the witness of non-uniformity
of `U` and `V`.  -/
SzemerediRegularity.star : {α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : DecidableEq α] →
      {P : Finpartition Finset.univ} →
        P.IsEquipartition →
          (G : SimpleGraph α) → [DecidableRel G.Adj] → ℝ → {U : Finset α} → U ∈ P.parts → Finset α → Finset (Finset α)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `K` and `Kᗮ` have trivial intersection.  -/
Submodule.inf_orthogonal_eq_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), K ⊓ Kᗮ = ⊥
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.topologicalClosure_map : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [inst_5 : ContinuousStar A] [inst_6 : ContinuousConstSMul R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : TopologicalSpace B] [inst_9 : Star B] [inst_10 : NonUnitalSemiring B]
  [inst_11 : Module R B] [inst_12 : IsSemitopologicalSemiring B] [inst_13 : ContinuousConstSMul R B]
  [inst_14 : ContinuousStar B] (s : NonUnitalStarSubalgebra R A) {φ : A →⋆ₙₐ[R] B},
  IsClosedMap ⇑φ →
    Continuous ⇑φ →
      (NonUnitalStarSubalgebra.map φ s).topologicalClosure = NonUnitalStarSubalgebra.map φ s.topologicalClosure
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.coeff_homogeneousComponent : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (p : ℕ) (d : σ →₀ ℕ) (f : MvPowerSeries σ R),
  (MvPowerSeries.coeff d) ((MvPowerSeries.homogeneousComponent p) f) =
    if Finsupp.degree d = p then (MvPowerSeries.coeff d) f else 0
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.div.eq_def : ∀ {v : Lean.Level} {M : Q(Type v)} (x x_1 : Mathlib.Tactic.FieldSimp.qNF M),
  x.div x_1 =
    match x, x_1 with
    | [], l => l.onExponent Neg.neg
    | l, [] => l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ > k₂ then ((a₁, x₁), k₁) :: Mathlib.Tactic.FieldSimp.qNF.div t₁ (((a₂, x₂), k₂) :: t₂)
      else
        if k₁ = k₂ then ((a₁ - a₂, x₁), k₁) :: Mathlib.Tactic.FieldSimp.qNF.div t₁ t₂
        else ((-a₂, x₂), k₂) :: Mathlib.Tactic.FieldSimp.qNF.div (((a₁, x₁), k₁) :: t₁) t₂
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.local.sizeOf_spec : ∀ (id : Lean.Name), sizeOf (Lean.Meta.Grind.Origin.local id) = 1 + sizeOf id
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam_one : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : One α], Metric.diam 1 = 0
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.anyM.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- Comparison test of convergence of series of non-negative real numbers.  -/
Summable.of_nonneg_of_le : ∀ {β : Type u_2} {f g : β → ℝ}, (∀ (b : β), 0 ≤ g b) → (∀ (b : β), g b ≤ f b) → Summable f → Summable g
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedFunctionTheorems : Inhabited Mathlib.Meta.FunProp.FunctionTheorems
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.prodMap_comap_prod : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {G' : Type u_8} {N' : Type u_9}
  [inst_2 : AddGroup G'] [inst_3 : AddGroup N'] (f : G →+ N) (g : G' →+ N') (S : AddSubgroup N) (S' : AddSubgroup N'),
  AddSubgroup.comap (f.prodMap g) (S.prod S') = (AddSubgroup.comap f S).prod (AddSubgroup.comap g S')
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.keys_insertIfNew_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {k : α}, (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys)
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β}, f.NeBot → g.NeBot → (f +ᵥ g).NeBot
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Measure.toTemperedDistribution_apply : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : SecondCountableTopology E] (μ : autoParam (MeasureTheory.Measure E) _auto_31✝)
  [hμ : μ.HasTemperateGrowth] (g : SchwartzMap E ℂ), μ.toTemperedDistribution g = ∫ (x : E), g x ∂μ
-- Mathlib.Analysis.Analytic.Basic
/-- If `f` has formal power series `∑ n, pₙ` in a set, within a ball of radius `r`, then
for `y, z` in any smaller ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is
bounded above by `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. This lemma formulates this property
using `IsBigO` and `Filter.principal` on `E × E`.  -/
HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal : ∀ {𝕜 : 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}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r r' : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    r' < r →
      (fun y =>
          f y.1 - f y.2 -
            (p 1) fun x => y.1 - y.2) =O[Filter.principal (Metric.eball (x, x) r' ∩ insert x s ×ˢ insert x s)]
        fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ] (f : β →Co γ)
  (g : α →Co β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The image of `canonicalEmbedding` lives in the `ℝ`-submodule of the `x ∈ ((K →+* ℂ) → ℂ)` such
that `conj x_φ = x_(conj φ)` for all `φ : K →+* ℂ`.  -/
NumberField.canonicalEmbedding.conj_apply : ∀ {K : Type u_1} [inst : Field K] {x : (K →+* ℂ) → ℂ} (φ : K →+* ℂ),
  x ∈ Submodule.span ℝ (Set.range ⇑(NumberField.canonicalEmbedding K)) →
    (starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α}, m.isEmpty = true → m.get? a = none
-- Mathlib.Data.Set.Pairwise.Lattice
Set.pairwiseDisjoint_iff : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s : Set ι},
  s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j
-- Mathlib.Data.Set.Inclusion
Set.val_comp_inclusion : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t), Subtype.val ∘ Set.inclusion h = Subtype.val
-- Mathlib.Topology.MetricSpace.Completion
Isometry.mapRingHom.congr_simp : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Ring α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α] [inst_4 : Ring β] [inst_5 : PseudoMetricSpace β] [inst_6 : IsUniformAddGroup β]
  [inst_7 : IsTopologicalRing β] {f f_1 : α →+* β} (e_f : f = f_1) (h : Isometry ⇑f), h.mapRingHom = ⋯.mapRingHom
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.next : ∀ {m₁ : List Char} {c : Char} {m₂ : List Char} {s : Substring.Raw},
  s.Valid →
    s.toString.toList = m₁ ++ c :: m₂ →
      s.next { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + c.utf8Size }
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.add : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E}, LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf + Kg) fun x => f x + g x
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.MatcherKey.mk.injEq : ∀ (value : Lean.Expr) (compile isPrivate : Bool) (value_1 : Lean.Expr) (compile_1 isPrivate_1 : Bool),
  ({ value := value, compile := compile, isPrivate := isPrivate } =
      { value := value_1, compile := compile_1, isPrivate := isPrivate_1 }) =
    (value = value_1 ∧ compile = compile_1 ∧ isPrivate = isPrivate_1)
-- Mathlib.Algebra.Category.MonCat.Basic
addEquivIsoAddMonCatIso.eq_1 : ∀ {X Y : Type u} [inst : AddMonoid X] [inst_1 : AddMonoid Y],
  addEquivIsoAddMonCatIso =
    { hom := TypeCat.ofHom fun e => e.toAddMonCatIso, inv := TypeCat.ofHom fun i => i.addMonCatIsoToAddEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- For a simplex, the centroid, a vertex, and the corresponding `faceOppositeCentroid` are
collinear.  -/
Affine.Simplex.collinear_point_centroid_faceOppositeCentroid : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [CharZero k] {n : ℕ} [inst_5 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  Collinear k {s.points i, s.centroid, s.faceOppositeCentroid i}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.evalEval_polynomialX_zero : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R}, Polynomial.evalEval 0 0 W.polynomialX = -W.a₄
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_natCast : ∀ {r : ℝ} {n : ℕ}, ENNReal.ofReal r ≤ ↑n ↔ r ≤ ↑n
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.map_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.map F).obj X =
    match X with
    | CategoryTheory.WithTerminal.of x => CategoryTheory.WithTerminal.of (F.obj x)
    | CategoryTheory.WithTerminal.star => CategoryTheory.WithTerminal.star
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorph.localInverseAt.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f f_1 : X → Y}
  (e_f : f = f_1) (hf : IsLocalHomeomorph f) (x x_1 : X), x = x_1 → hf.localInverseAt x = ⋯.localInverseAt x_1
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- In the specific case of continuous alternating maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `Π(i : Fin (n+1)), M i` using `cons`, one can express directly the
additivity of an alternating map along the first variable.  -/
ContinuousAlternatingMap.cons_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N] {n : ℕ}
  (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (x y : M), f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.object : Lean.Lsp.SymbolKind
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_congr : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {k₁ k₂ : α}, (k₁ == k₂) = true → m.getKey! k₁ = m.getKey! k₂
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_iff_forall_isBigOWith`.

---

Definition of `IsLittleO` in terms of `IsBigOWith`.  -/
Asymptotics.IsLittleO.of_isBigOWith : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  (∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g) → f =o[l] g
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.check.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.check e) = 1 + sizeOf e
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.instIsGaussianMapHAdd : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] (c : E),
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (fun x => x + c) μ)
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
_private.Mathlib.Algebra.Category.ModuleCat.Biproducts.0.lequivProdOfRightSplitExact' : {R : Type u} →
  {A M B : Type v} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup A] →
        [inst_2 : Module R A] →
          [inst_3 : AddCommGroup B] →
            [inst_4 : Module R B] →
              [inst_5 : AddCommGroup M] →
                [inst_6 : Module R M] →
                  {j : A →ₗ[R] M} →
                    {g : M →ₗ[R] B} →
                      {f : B →ₗ[R] M} →
                        Function.Injective ⇑j → j.range = g.ker → g ∘ₗ f = LinearMap.id → (A × B) ≃ₗ[R] M
-- Mathlib.GroupTheory.Finiteness
/-- Finite product of finitely generated monoids is finitely generated.  -/
Pi.instMonoidFG : ∀ {ι : Type u_5} [Finite ι] {M : ι → Type u_6} [inst : (i : ι) → Monoid (M i)] [∀ (i : ι), Monoid.FG (M i)],
  Monoid.FG ((i : ι) → M i)
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_zero_right : ∀ {R : Type u_1} [inst : CommRing R] (a : Polynomial R), a.wronskian 0 = 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.im.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj),
  CategoryTheory.Subgroupoid.im φ hφ = CategoryTheory.Subgroupoid.map φ hφ ⊤
-- Mathlib.Algebra.Prime.Lemmas
Prime.not_isSquare : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : M}, Prime p → ¬IsSquare p
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.createsColimitsOfShape : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {G : CategoryTheory.Functor A T} →
              {X : T} →
                [CategoryTheory.Limits.PreservesColimitsOfShape J G] →
                  CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.CostructuredArrow.proj G X)
-- Mathlib.Topology.Convenient.Category
/-- Let `X i` be a family of topological spaces. This is the type of objects
in a category ` ContinuousGeneratedByCat X` where:
* objects are topological spaces;
* morphisms are `X`-continuous maps.  -/
ContinuousGeneratedByCat : {ι : Type t} → (X : ι → Type u) → [(i : ι) → TopologicalSpace (X i)] → Type (v + 1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_alterKey' : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
  {l : List ((a : α) × β a)},
  (Std.Internal.List.alterKey k f l).length =
    if Std.Internal.List.containsKey k l = true ∧ (f (Std.Internal.List.getValueCast? k l)).isNone = true then
      l.length - 1
    else
      if Std.Internal.List.containsKey k l = false ∧ (f (Std.Internal.List.getValueCast? k l)).isSome = true then
        l.length + 1
      else l.length
-- Lean.LibrarySuggestions.Basic
Lean.MVarId.getRelevantConstants : Lean.MVarId → Lean.MetaM Lean.NameSet
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], (m₁ ∩ m₂)[k]! = if k ∈ m₂ then m₁[k]! else default
-- Init.Data.List.Count
List.count_replicate : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {n : ℕ},
  List.count a (List.replicate n b) = if (b == a) = true then n else 0
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The monad for the normalization of 2-morphisms.  -/
Mathlib.Tactic.Bicategory.BicategoryM : Type → Type
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!.eq_1 : ∀ {α : Type u} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (l : ρ),
  Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun a __s =>
            let r := __s;
            have r := ⟨Std.DTreeMap.Internal.Impl.insertIfNew! a () ↑r, ⋯⟩;
            pure (ForInStep.yield r)
      have r : Std.DTreeMap.Internal.Impl.Const.IteratedSlowUnitInsertionInto t := __s
      pure r).run
-- Mathlib.Data.Finsupp.Single
Finsupp.apply_surjective : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α), Function.Surjective fun f => f a
-- Mathlib.Data.Sum.Order
OrderIso.sumLexAssoc_apply_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (c : γ),
  (OrderIso.sumLexAssoc α β γ) (toLex (Sum.inr c)) = toLex (Sum.inr (toLex (Sum.inr c)))
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- A point `p` is equidistant to two affine subspaces (typically lines, for this version of the
lemma) if the oriented angles at a point `p'` in their intersection between `p` and its orthogonal
projections onto the subspaces are equal.  -/
EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂),
  ↑((EuclideanGeometry.orthogonalProjection s₁) p) ≠ p' →
    ↑((EuclideanGeometry.orthogonalProjection s₂) p) ≠ p' →
      EuclideanGeometry.oangle (↑((EuclideanGeometry.orthogonalProjection s₁) p)) p' p =
          EuclideanGeometry.oangle p p' ↑((EuclideanGeometry.orthogonalProjection s₂) p) →
        dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) =
          dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p)
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.coe_mkUnit : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] {a : kˣ}
  {A : WittVector p k} (hA : A.coeff 0 = ↑a), ↑(WittVector.mkUnit hA) = A
-- Std.Http.Protocol.H1.Reader
/-- Adds header bytes accumulated for the current message.
 -/
Std.Http.Protocol.H1.Reader.addHeaderBytes : {dir : Std.Http.Protocol.H1.Direction} → ℕ → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Data.Int.Interval
Int.card_fintype_Ioc_of_le : ∀ (a b : ℤ), a ≤ b → ↑(Fintype.card ↑(Set.Ioc a b)) = b - a
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat.inj : ∀ {a b : Lean.Expr} {natStructId : ℕ} {la lb : Lean.Meta.Grind.Arith.Linear.LinExpr} {a_1 b_1 : Lean.Expr}
  {natStructId_1 : ℕ} {la_1 lb_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat a b natStructId la lb =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat a_1 b_1 natStructId_1 la_1 lb_1 →
    a = a_1 ∧ b = b_1 ∧ natStructId = natStructId_1 ∧ la = la_1 ∧ lb = lb_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_union! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.union! m₂) k fallback =
          Std.DTreeMap.Internal.Impl.Const.getD m₂ k (Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback)