mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.MaxPowDiv
/-- **Alias** of the reverse direction of `Nat.pow_dvd_iff_le_padicValNat`.

---

If `p > 1`, `n > 0`, then the first component of `maxPowDvdDiv` is the maximal power of `p`
that divides `n`.  -/
Nat.maxPowDiv.le_of_dvd : ∀ {p k n : ℕ}, p ≠ 1 → n ≠ 0 → k ≤ padicValNat p n → p ^ k ∣ n
-- Batteries.Data.Vector.Lemmas
Vector.get_cast : ∀ {α : Type u_1} {m n : ℕ} (v : Vector α m) (h : m = n) (i : Fin n), (Vector.cast h v).get i = v.get (Fin.cast ⋯ i)
-- Mathlib.FieldTheory.Perfect
PerfectRing.one : ∀ (M : Type u_1) [inst : CommMonoid M], PerfectRing M 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
/-- For `a ≤ b`, there is a `c` so `b = a + c`.  -/
ExistsAddOfLE.exists_add_of_le : ∀ {α : Type u} {inst : Add α} {inst_1 : LE α} [self : ExistsAddOfLE α] {a b : α}, a ≤ b → ∃ c, b = a + c
-- Init.Data.String.Defs
String.Pos.ext_iff : ∀ {s : String} {x y : s.Pos}, x = y ↔ x.offset = y.offset
-- Mathlib.Computability.Primrec.Basic
Primrec₂.uncurry : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, Primrec (Function.uncurry f) ↔ Primrec₂ f
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- `select m n` runs `right` `m` times; if `m < n`, then it also runs `left` once.
Fails if `n < m`.  -/
_private.Mathlib.Tactic.MkIffOfInductiveProp.0.Mathlib.Tactic.MkIff.select : ℕ → ℕ → Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.reindex_toLimitPresentation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J'] {X : C}
  (h : P.LimitOfShape J X) (G : CategoryTheory.Functor J' J) [inst_3 : G.Initial],
  (h.reindex G).toLimitPresentation = h.reindex G
-- Mathlib.GroupTheory.OrderOfElement
AddSubmonoid.addOrderOf_le_card : ∀ {G : Type u_6} [inst : AddGroup G] (s : AddSubmonoid G), (↑s).Finite → ∀ {x : G}, x ∈ s → addOrderOf x ≤ Nat.card ↥s
-- Lean.Data.Trie
Lean.Data.Trie.brecOn.go : {α : Type} →
  {motive_1 : Lean.Data.Trie α → Sort u} →
    {motive_2 : Array (Lean.Data.Trie α) → Sort u} →
      {motive_3 : List (Lean.Data.Trie α) → Sort u} →
        (t : Lean.Data.Trie α) →
          ((t : Lean.Data.Trie α) → t.below → motive_1 t) →
            ((t : Array (Lean.Data.Trie α)) → Lean.Data.Trie.below_1 t → motive_2 t) →
              ((t : List (Lean.Data.Trie α)) → Lean.Data.Trie.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.sub_ae_eq_zero : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : AddGroup β]
  (f g : α → β), f - g =ᵐ[μ] 0 ↔ f =ᵐ[μ] g
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_pairSep : ∀ {p : ZFSet.{u} → ZFSet.{u} → Prop} {x y z : ZFSet.{u}},
  z ∈ ZFSet.pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b
-- Mathlib.RepresentationTheory.Induced
Representation.ind_mk : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  {A : Type u_4} [inst_3 : AddCommGroup A] [inst_4 : Module k A] (ρ : Representation k G A) (h₁ h₂ : H) (a : A),
  ((Representation.ind φ ρ) h₁) ((Representation.IndV.mk φ ρ h₂) a) = (Representation.IndV.mk φ ρ (h₂ * h₁⁻¹)) a
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Given a Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and another morphism
`φ' : a' ⟶ b` which also lifts `f`, then `IsCartesian.map f φ φ'` is the morphism `a' ⟶ a` lifting
`𝟙 R` obtained from the universal property of `φ`.  -/
CategoryTheory.Functor.IsCartesian.map : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          {R S : 𝒮} →
            {a b : 𝒳} →
              (f : R ⟶ S) → (φ : a ⟶ b) → [p.IsCartesian f φ] → {a' : 𝒳} → (φ' : a' ⟶ b) → [p.IsHomLift f φ'] → a' ⟶ a
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.piEquiv_symm_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M₁ i)]
  [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : (i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι' → Type u_2}
  [inst_4 : (i : ι') → AddCommMonoid (M' i)] [inst_5 : (i : ι') → TopologicalSpace (M' i)]
  [inst_6 : (i : ι') → Module R (M' i)] (f : ContinuousMultilinearMap R M₁ ((i : ι') → M' i)) (i : ι'),
  ContinuousMultilinearMap.piEquiv.symm f i = (ContinuousLinearMap.proj i).compContinuousMultilinearMap f
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsInertiaField.toIsGaloisGroup : ∀ {K : Type u_2} {L : Type u_3} {B : Type u_4} {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L}
  {inst_3 : CommRing B} {P : Ideal B} {E : Type u_6} {inst_4 : Field E} {inst_5 : Algebra E L}
  {inst_6 : MulSemiringAction Gal(L/K) B} [self : IsInertiaField K L P E],
  IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) E L
-- Mathlib.Analysis.Complex.Basic
Complex.conjCAE_toAlgEquiv : Complex.conjCAE.toAlgEquiv = Complex.conjAe
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A version of `WithTop.map` for `AddMonoidHom`s.  -/
AddMonoidHom.withTopMap : {M : Type u_1} →
  {N : Type u_2} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (M →+ N) → WithTop M →+ WithTop N
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- **Alias** of `Complex.UnitDisc.coe_star`. -/
Complex.UnitDisc.coe_conj : ∀ (z : Complex.UnitDisc), ↑(star z) = (starRingEnd ℂ) ↑z
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instZero : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → Zero (MeasureTheory.FiniteMeasure Ω)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
DiscreteMeasurableSpace.toBorelSpace : ∀ {α : Type u_6} [inst : TopologicalSpace α] [DiscreteTopology α] [inst_2 : MeasurableSpace α]
  [DiscreteMeasurableSpace α], BorelSpace α
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.of_small : ∀ {L : FirstOrder.Language} {T : L.Theory} (M : Type w) [inst : Nonempty M] [inst_1 : L.Structure M] [inst_2 : M ⊨ T]
  [h : Small.{w', w} M], Small.{w', w} ↑(FirstOrder.Language.Theory.ModelType.of T M)
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Lebesgue dominated convergence theorem provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
`setToFun`.
We could weaken the condition `bound_integrable` to require `HasFiniteIntegral bound μ` instead
(i.e. not requiring that `bound` is measurable), but in all applications proving integrability
is easier.  -/
MeasureTheory.tendsto_setToFun_of_dominated_convergence : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : ℕ → α → E} {f : α → E}
  (bound : α → ℝ),
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ) →
    MeasureTheory.Integrable bound μ →
      (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => fs n a) Filter.atTop (nhds (f a))) →
          Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT (fs n)) Filter.atTop
            (nhds (MeasureTheory.setToFun μ T hT f))
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.mk.injEq : ∀ (elimApp : Lean.Expr) (elimArgs : Array Lean.Expr) (motive : Lean.MVarId) (alts : Array Lean.Elab.Tactic.ElimApp.Alt)
  (others : Array Lean.MVarId) (complexArgs : Array Lean.Expr) (elimApp_1 : Lean.Expr) (elimArgs_1 : Array Lean.Expr)
  (motive_1 : Lean.MVarId) (alts_1 : Array Lean.Elab.Tactic.ElimApp.Alt) (others_1 : Array Lean.MVarId)
  (complexArgs_1 : Array Lean.Expr),
  ({ elimApp := elimApp, elimArgs := elimArgs, motive := motive, alts := alts, others := others,
        complexArgs := complexArgs } =
      { elimApp := elimApp_1, elimArgs := elimArgs_1, motive := motive_1, alts := alts_1, others := others_1,
        complexArgs := complexArgs_1 }) =
    (elimApp = elimApp_1 ∧
      elimArgs = elimArgs_1 ∧ motive = motive_1 ∧ alts = alts_1 ∧ others = others_1 ∧ complexArgs = complexArgs_1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentEdit.mk.inj : ∀ {textDocument : Lean.Lsp.VersionedTextDocumentIdentifier} {edits : Lean.Lsp.TextEditBatch}
  {textDocument_1 : Lean.Lsp.VersionedTextDocumentIdentifier} {edits_1 : Lean.Lsp.TextEditBatch},
  { textDocument := textDocument, edits := edits } = { textDocument := textDocument_1, edits := edits_1 } →
    textDocument = textDocument_1 ∧ edits = edits_1
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.zero_smul : ∀ {ιA : Type u_1} {ιB : Type u_2} {A : ιA → Type u_3} {M : ιB → Type u_4} {inst : AddMonoid ιA} {inst_1 : VAdd ιA ιB}
  {inst_2 : (i : ιA) → AddMonoid (A i)} {inst_3 : (i : ιB) → AddMonoid (M i)} {inst_4 : GradedMonoid.GMonoid A}
  [self : DirectSum.Gmodule A M] {i : ιA} {j : ιB} (b : M j), GradedMonoid.GSMul.smul 0 b = 0
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.isOrdinal_toZFSet : ∀ (o : Ordinal.{u_1}), o.toZFSet.IsOrdinal
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.instZero : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        {φ : R →* S} →
          {A : Type v} →
            {B : Type w} →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] → [inst_5 : DistribMulAction S B] → Zero (A →ₛₙₐ[φ] B)
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation from an emetric space is injective  -/
Dilation.injective : ∀ {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace β] {α : Type u_5} [inst_1 : EMetricSpace α]
  [inst_2 : FunLike F α β] [DilationClass F α β] (f : F), Function.Injective ⇑f
-- Mathlib.Order.RelIso.Basic
/-- A relation isomorphism between equal relations on equal types.  -/
RelIso.cast : {α β : Type u} → {r : α → α → Prop} → {s : β → β → Prop} → α = β → r ≍ s → r ≃r s
-- Mathlib.Order.Filter.IsBounded
Filter.not_isBoundedUnder_of_tendsto_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α} [l.NeBot],
  Filter.Tendsto f l Filter.atTop → ¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_ne_zero : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), x.denom ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The map `(· * f)`.  -/
CategoryTheory.GrpObj.mulRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A : C} → [CategoryTheory.GrpObj A] → (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A) → (A ≅ A)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight.inj : ∀ {c₁ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr} {c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr}
  {c₁_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr} {c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.negDvdTight c₁_1 c₂_1 →
    c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- The space of multilinear maps on `Π (i : Fin (n+1)), M i` is canonically isomorphic to
the space of linear maps from the space of multilinear maps on `Π (i : Fin n), M (castSucc i)` to
the space of linear maps on `M (last n)`, by separating the last variable. We register this
isomorphism as a linear isomorphism in `multilinearCurryRightEquiv R M M₂`.

The direct and inverse maps are given by `f.curryRight` and `f.uncurryRight`. Use these
unless you need the full framework of linear equivs.  -/
multilinearCurryRightEquiv : (R : Type uR) →
  {n : ℕ} →
    (M : Fin n.succ → Type v) →
      (M₂ : Type v₂) →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] →
                  MultilinearMap R M M₂ ≃ₗ[R] MultilinearMap R (fun i => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.ShortComplex.mono_of_mono_of_mono_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ShortComplex C} (φ : R₁ ⟶ R₂),
  R₁.Exact → CategoryTheory.Mono R₂.f → CategoryTheory.Mono φ.τ₁ → CategoryTheory.Mono φ.τ₃ → CategoryTheory.Mono φ.τ₂
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j k : n) (r : R),
  (LieAlgebra.SpecialLinear.singleSubSingle i j) r + (LieAlgebra.SpecialLinear.singleSubSingle j k) r =
    (LieAlgebra.SpecialLinear.singleSubSingle i k) r
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.pow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {s : 𝕜 → 𝕜'} {U : Set 𝕜}, MeromorphicOn s U → ∀ (n : ℕ), MeromorphicOn (s ^ n) U
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instMonadExceptExceptionGrindTacticM : MonadExcept Lean.Exception Lean.Elab.Tactic.Grind.GrindTacticM
-- Init.Conv
/-- Executes the given conv block without converting regular goal into a `conv` goal.  -/
Lean.Parser.Tactic.Conv.convTactic : Lean.ParserDescr
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The initial object in `Factorisation f`, with the domain of `f` as its midpoint.  -/
CategoryTheory.Factorisation.initial : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Factorisation f
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasFDerivWithinAt.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_5}
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H}
  {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G},
  HasFDerivWithinAt c c' s x →
    HasFDerivWithinAt d d' s x →
      HasFDerivWithinAt (fun y => c y ∘SL d y)
        ((ContinuousLinearMap.compL 𝕜 F G H) (c x) ∘SL d' + (ContinuousLinearMap.compL 𝕜 F G H).flip (d x) ∘SL c') s x
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inductively defined smallest additive congruence relation containing a given binary
relation.  -/
AddConGen.Rel : {M : Type u_1} → [Add M] → (M → M → Prop) → M → M → Prop
-- Mathlib.Topology.Algebra.Module.Complement
/-- If `p` is a closed complemented submodule,
then there exists a submodule `q` and a continuous linear equivalence `M ≃L[R] (p × q)` such that
`e (x : p) = (x, 0)`, `e (y : q) = (0, y)`, and `e.symm x = x.1 + x.2`.

In fact, the properties of `e` imply the properties of `e.symm` and vice versa,
but we provide both for convenience.  -/
Submodule.ClosedComplemented.exists_submodule_equiv_prod : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [IsTopologicalAddGroup M] {p : Submodule R M},
  p.ClosedComplemented →
    ∃ q e, (∀ (x : ↥p), e ↑x = (x, 0)) ∧ (∀ (y : ↥q), e ↑y = (0, y)) ∧ ∀ (x : ↥p × ↥q), e.symm x = ↑x.1 + ↑x.2
-- Mathlib.Algebra.Notation.Indicator
Set.indicator.eq_1 : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (s : Set α) (f : α → M) (x : α),
  s.indicator f x = if x ∈ s then f x else 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
QuasispectrumRestricts.continuous_nonUnitalStarAlgHom : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S] [inst_6 : StarRing S]
  [inst_7 : MetricSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S] [inst_10 : NonUnitalRing A]
  [inst_11 : StarRing A] [inst_12 : Module S A] [inst_13 : IsScalarTower S A A] [inst_14 : SMulCommClass S A A]
  [inst_15 : Algebra R S] [inst_16 : Module R A] [inst_17 : IsScalarTower R S A] [inst_18 : StarModule R S]
  [inst_19 : ContinuousSMul R S] [inst_20 : TopologicalSpace A] {a : A}
  {φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A},
  Continuous ⇑φ →
    ∀ {f : C(S, R)} (h : QuasispectrumRestricts a ⇑f), Continuous ⇑(QuasispectrumRestricts.nonUnitalStarAlgHom φ h)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.add.inj : ∀ {a b a_1 b_1 : Nat.Internal.Linear.Expr}, a.add b = a_1.add b_1 → a = a_1 ∧ b = b_1
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.category_comp_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (α : X.Hom Y)
  (β : Y.Hom Z) (x : X.I),
  (CategoryTheory.CategoryStruct.comp α β).φ x = CategoryTheory.CategoryStruct.comp (α.φ x) (β.φ (α.f x))
-- Mathlib.Algebra.Group.Action.End
/-- Given groups `G H` with `G` acting on `A`, `G` acts by
multiplicative automorphisms on `A → H`.  -/
mulAutArrow : {G : Type u_1} →
  {M : Type u_2} → {A : Type u_4} → [inst : Group G] → [MulAction G A] → [inst_2 : Monoid M] → G →* MulAut (A → M)
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.evalRingHom_zero : Polynomial.evalRingHom 0 = Polynomial.constantCoeff
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_fdiv_le_natAbs : ∀ (a b : ℤ), (a.fdiv b).natAbs ≤ a.natAbs
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.num.inj : ∀ {k k_1 : ℤ}, Lean.Grind.CommRing.Poly.num k = Lean.Grind.CommRing.Poly.num k_1 → k = k_1
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.aeval_eq_constantCoeff_of_vars : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {g : σ → S} {p : MvPolynomial σ R},
  (∀ i ∈ p.vars, g i = 0) → (MvPolynomial.aeval g) p = (algebraMap R S) (MvPolynomial.constantCoeff p)
-- Lean.Meta.Basic
Lean.Meta.DefEqContext.lctx : Lean.Meta.DefEqContext → Lean.LocalContext
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.IsLimit.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I}
  (hK : CategoryTheory.Limits.IsLimit K) {T : C} {f g : T ⟶ K.pt},
  (∀ (a : J.L), CategoryTheory.CategoryStruct.comp f (K.ι a) = CategoryTheory.CategoryStruct.comp g (K.ι a)) → f = g
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion.0.iteratedDerivWithin_cexp_aux : ∀ (k m : ℕ) (p : ℝ) {S : Set ℂ},
  IsOpen S →
    Set.EqOn (iteratedDerivWithin k (fun s => Complex.exp (2 * ↑Real.pi * Complex.I * ↑m * s / ↑p)) S)
      (fun s => (2 * ↑Real.pi * Complex.I * ↑m / ↑p) ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑m * s / ↑p)) S
-- Mathlib.Data.Matrix.Basic
RingHom.mapMatrix_comp : ∀ {m : Type u_2} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonAssocSemiring α] [inst_3 : NonAssocSemiring β] [inst_4 : NonAssocSemiring γ] (f : β →+* γ) (g : α →+* β),
  f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.homOfLE_app_val : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) (Δ : SimplexCategoryᵒᵖ) (x : ↑(S₁.obj Δ)),
  ↑((CategoryTheory.ConcreteCategory.hom ((SSet.Subcomplex.homOfLE h).app Δ)) x) = ↑x
-- Mathlib.Order.Category.DistLat
DistLat.str : (self : DistLat) → DistribLattice ↑self
-- Mathlib.Algebra.GroupWithZero.Range
/-- See also `mem_valueGroup_iff_of_comm'` for a version proving that `f x ≠ 0`.  -/
MonoidWithZeroHom.mem_valueGroup_iff_of_comm : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B) {y : Bˣ},
  y ∈ f.valueGroup ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls.match_4.eq_2 : ∀ (motive : Option (Lean.Expr × Subarray Lean.Expr) → Sort u_1) (origParam : Lean.Expr) (s' : Subarray Lean.Expr)
  (h_1 : Unit → motive none)
  (h_2 : (origParam : Lean.Expr) → (s' : Subarray Lean.Expr) → motive (some (origParam, s'))),
  (match some (origParam, s') with
    | none => h_1 ()
    | some (origParam, s') => h_2 origParam s') =
    h_2 origParam s'
-- Init.Data.String.Basic
String.Pos.ofToSlice_lt_iff : ∀ {s : String} {p : s.toSlice.Pos} {q : s.Pos}, String.Pos.ofToSlice p < q ↔ p < q.toSlice
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.isMulCommutative : ∀ {G : Type u_1} [inst : Group G] [IsKleinFour G], IsMulCommutative G
-- Mathlib.Data.List.Triplewise
List.triplewise_append : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → α → α → Prop},
  List.Triplewise p (l₁ ++ l₂) ↔
    List.Triplewise p l₁ ∧
      List.Triplewise p l₂ ∧ (∀ a ∈ l₁, List.Pairwise (p a) l₂) ∧ ∀ a ∈ l₂, List.Pairwise (fun x y => p x y a) l₁
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P]
  (i : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : d.glued.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (d.pullbackGluedIso i).inv.left
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst d.glued.hom (𝒰.f i)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i) h
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
/-- the maps `unitary.argSelfAdjoint` and `selfAdjoint.expUnitary` form a partial
homeomorphism between `ball (1 : unitary A) 2` and `ball (0 : selfAdjoint A) π`.  -/
Unitary.openPartialHomeomorph : {A : Type u_1} → [inst : CStarAlgebra A] → OpenPartialHomeomorph ↥(unitary A) ↥(selfAdjoint A)
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- For every bound `B`, a ring with finite quotients has only finitely many ideals of norm bounded
by `B`.  -/
Ring.HasFiniteQuotients.finite_cardQuot_le : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R] (B : ℕ), {I | Submodule.cardQuot I ≤ B}.Finite
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.isPushout_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  sq.IsPushout ↔ Nonempty (CategoryTheory.Limits.IsColimit sq.pushoutCocone)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_neg_vadd_union : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ ((-c +ᵥ s) ∪ t) = μ (s ∪ (c +ᵥ t))