mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.PrimesInAP
_private.Mathlib.NumberTheory.LSeries.PrimesInAP.0.ArithmeticFunction.vonMangoldt.F₀ : ℕ → ℝ
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_functor_map_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) {X Y : CategoryTheory.MorphismProperty.Comma L₁ R P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).functor.map f).right =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).right
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation_sup : ∀ {M : Type u_1} [inst : AddZeroClass M] {s₁ s₂ : AddSubmonoid M}, (s₁ ⊔ s₂).saturation = s₁.saturation ⊔ s₂.saturation
-- Mathlib.Data.Nat.PrimeFin
Nat.Prime.mem_primeFactors_self : ∀ {p : ℕ}, Nat.Prime p → p ∈ p.primeFactors
-- Init.Data.Array.Zip
Array.zipWith_eq_zipWith_take_min : ∀ {α : Type u_1} {β : Type u_2} {α_1 : Type u_3} {f : α → β → α_1} (as : Array α) (bs : Array β),
  Array.zipWith f as bs = Array.zipWith f (as.take (min as.size bs.size)) (bs.take (min as.size bs.size))
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.pow : ∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
  [inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {f : α → β} {g : α → γ},
  Measurable f → Measurable g → Measurable fun x => f x ^ g x
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_pow_mul_natDegree : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instRightCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : RightCancelMonoid α],
  OrderDual.instRightCancelMonoid = { toMonoid := OrderDual.instMonoid, toIsRightCancelMul := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_top : ∀ {G : Type u_1} [inst : AddGroup G], ↑⊤ = Set.univ
-- Mathlib.Topology.Category.TopCat.ULift
/-- The functor which sends a topological space in `Type u` to a homeomorphic
space in `Type (max u v)`.  -/
TopCat.uliftFunctor : CategoryTheory.Functor TopCat TopCat
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_le_pow_left' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {a b : M},
  a ≤ b → ∀ (i : ℕ), a ^ i ≤ b ^ i
-- Mathlib.Order.Category.PartOrdEmb
/-- A colimit cocone for `F : J ⥤ PartOrdEmb` (with `J` filtered) can be
obtained from a colimit cocone for `F ⋙ forget _`.  -/
PartOrdEmb.Limits.isColimitCocone : {J : Type u} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      {F : CategoryTheory.Functor J PartOrdEmb} →
        {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} →
          (hc : CategoryTheory.Limits.IsColimit c) → CategoryTheory.Limits.IsColimit (PartOrdEmb.Limits.cocone hc)
-- Init.Data.List.Monadic
List.mapM_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β}
  {g : β → m γ} {l : List α}, List.mapM g (List.map f l) = List.mapM (g ∘ f) l
-- Init.Data.Sum.Basic
Sum.instDecidableLiftRel : {α : Type u_1} →
  {γ : Type u_2} →
    {β : Type u_3} →
      {δ : Type u_4} →
        {r : α → γ → Prop} →
          {s : β → δ → Prop} →
            [(a : α) → (c : γ) → Decidable (r a c)] →
              [(b : β) → (d : δ) → Decidable (s b d)] → (ab : α ⊕ β) → (cd : γ ⊕ δ) → Decidable (Sum.LiftRel r s ab cd)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_reverse : ∀ {α : Type u_1} {a : FreeMonoid α}, a.reverse.length = a.length
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ιOrZero_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄), ⋯ ≠ j → ⋯ = ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.getRing? : Lean.Meta.Grind.Arith.Linear.LinearM (Option Lean.Meta.Grind.Arith.CommRing.Ring)
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_two : ∀ {R : Type u_1} [inst : Semiring R] {x : R}, ∑ i ∈ Finset.range 2, x ^ i = x + 1
-- Mathlib.RingTheory.AdicCompletion.Topology
AddGroupFilterBasis.mk.congr_simp : ∀ {A : Type u} [inst : AddGroup A] (toFilterBasis toFilterBasis_1 : FilterBasis A)
  (e_toFilterBasis : toFilterBasis = toFilterBasis_1) (zero' : ∀ {U : Set A}, U ∈ toFilterBasis.sets → 0 ∈ U)
  (add' : ∀ {U : Set A}, U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V + V ⊆ U)
  (neg' : ∀ {U : Set A}, U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V ⊆ (fun x => -x) ⁻¹' U)
  (conj' :
    ∀ (x₀ : A) {U : Set A}, U ∈ toFilterBasis.sets → ∃ V ∈ toFilterBasis.sets, V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U),
  { toFilterBasis := toFilterBasis, zero' := zero', add' := add', neg' := neg', conj' := conj' } =
    { toFilterBasis := toFilterBasis_1, zero' := ⋯, add' := ⋯, neg' := ⋯, conj' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt_conjSqrt_ringInverse : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] [IsSemitopologicalRing A] [T2Space A]
  (c a : A),
  autoParam (IsStrictlyPositive c) CFC.conjSqrt_conjSqrt_ringInverse._auto_1 →
    (CFC.conjSqrt c) ((CFC.conjSqrt (Ring.inverse c)) a) = a
-- Lean.DocString.Parser
/-- Like `satisfyFn`, but allows any escape sequence through  -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.satisfyEscFn : (Char → Bool) → optParam String "unexpected character" → Lean.Parser.ParserFn
-- Mathlib.Algebra.Algebra.Operations
Submodule.toSubMulAction_one : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A],
  Submodule.toSubMulAction 1 = 1
-- Mathlib.Data.Finset.Lattice.Fold
Finset.toDual_inf' : ∀ {α : Type u_2} {ι : Type u_5} [inst : SemilatticeInf α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α),
  OrderDual.toDual (s.inf' hs f) = s.sup' hs (⇑OrderDual.toDual ∘ f)
-- Mathlib.Order.KrullDimension
Order.coheight_anti : ∀ {α : Type u_1} [inst : Preorder α], Antitone Order.coheight
-- Mathlib.Data.Matrix.Basis
/-- `Matrix.single` as a bundled linear map.  -/
Matrix.singleLinearMap : {m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_5) →
      {α : Type u_7} →
        [DecidableEq m] →
          [DecidableEq n] →
            [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [inst_2 : Module R α] → m → n → α →ₗ[R] Matrix m n α
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Return the Interfaces for rewriting `e`, both filtered and unfiltered.  -/
Mathlib.Tactic.LibraryRewrite.getRewriteInterfaces : Lean.Expr →
  Option ℕ →
    Option Lean.Name →
      Option Lean.FVarId →
        Lean.Lsp.Range →
          Lean.MetaM
            (Array (Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind) ×
              Array (Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind))
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The linear equivalence `M ≃ₗ[R] ⋀[R]^1 M`.  -/
exteriorPower.oneEquiv : (R : Type u) →
  [inst : CommRing R] → (M : Type u_1) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ↥(⋀[R]^1 M) ≃ₗ[R] M
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseLeapSecond : Std.Internal.Parsec.ByteArray.Parser ℤ → Std.Internal.Parsec.ByteArray.Parser Std.Time.TimeZone.TZif.LeapSecond
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.constGetThenInsertIfNew? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {a : α} {b : β}, t.WF → (Std.DTreeMap.Raw.Const.getThenInsertIfNew? t a b).2.WF
-- Mathlib.Algebra.GroupWithZero.Associated
dvdNotUnit_of_dvdNotUnit_associated : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q r : M}, DvdNotUnit p q → Associated q r → DvdNotUnit p r
-- Init.Data.Range.Polymorphic.Char
_private.Init.Data.Range.Polymorphic.Char.0.Char.instPreservesRxcSizeFinNumCodePointsMap : Char.map✝.PreservesRxcSize
-- Init.PropLemmas
and_left_comm : ∀ {a b c : Prop}, a ∧ b ∧ c ↔ b ∧ a ∧ c
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The `plusPart` of a subset `A` of the `mixedSpace` is the set of points in `A` that are
positive at all real places.  -/
NumberField.mixedEmbedding.plusPart : {K : Type u_1} →
  [inst : Field K] → Set (NumberField.mixedEmbedding.mixedSpace K) → Set (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  ∀ i ∉ Set.range P.map, P.sectionCotangent (P.cotangentSpaceBasis i) = 0
-- Batteries.Data.DList.Lemmas
_private.Batteries.Data.DList.Lemmas.0.Batteries.DList.append.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.DList α → Batteries.DList α → Sort u_2) (f : List α → List α)
  (h₁ : ∀ (l : List α), f l = f [] ++ l) (g : List α → List α) (h₂ : ∀ (l : List α), g l = g [] ++ l)
  (h_1 :
    (f : List α → List α) →
      (h₁ : ∀ (l : List α), f l = f [] ++ l) →
        (g : List α → List α) →
          (h₂ : ∀ (l : List α), g l = g [] ++ l) →
            motive { apply := f, invariant := h₁ } { apply := g, invariant := h₂ }),
  (match { apply := f, invariant := h₁ }, { apply := g, invariant := h₂ } with
    | { apply := f, invariant := h₁ }, { apply := g, invariant := h₂ } => h_1 f h₁ g h₂) =
    h_1 f h₁ g h₂
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict_id_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y), (f.restrict f.domain ⋯ ⋯).hom = f.hom
-- Mathlib.Data.Nat.Bitwise
/-- Proving associativity of bitwise operations in general essentially boils down to a huge case
distinction, so it is shorter to use this tactic instead of proving it in the general case.  -/
Nat.tacticBitwise_assoc_tac : Lean.ParserDescr
-- Init.Tactics
/-- `mexists` is like `exists`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mexists 42
```
 -/
Lean.Parser.Tactic.mexistsMacro : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- `Function.const` as a `MonoidHom`.  -/
Pi.constMonoidHom : (α : Type u_5) → (β : Type u_6) → [inst : MulOneClass β] → β →* α → β
-- Init.SimpLemmas
not_and : ∀ {a b : Prop}, ¬(a ∧ b) ↔ a → ¬b
-- Lean.Meta.Tactic.Assert
Lean.Meta.Hypothesis : Type
-- Init.Data.List.Basic
/-- Auxiliary for `splitAt`:
`splitAt.go l xs n acc = (acc.reverse ++ take n xs, drop n xs)` if `n < xs.length`,
and `(l, [])` otherwise.
 -/
List.splitAt.go : {α : Type u} → List α → List α → ℕ → List α → List α × List α
-- Mathlib.Data.List.Permutation
List.map_map_permutations'Aux : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : α) (ts : List α),
  List.map (List.map f) (List.permutations'Aux t ts) = List.permutations'Aux (f t) (List.map f ts)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Cache.WF.below.push_id : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α]
  {motive :
    (a : Array (Std.Sat.AIG.Decl α)) → (a_1 : Std.HashMap (Std.Sat.AIG.Decl α) ℕ) → Std.Sat.AIG.Cache.WF a a_1 → Prop}
  {decls : Array (Std.Sat.AIG.Decl α)} {cache : Std.HashMap (Std.Sat.AIG.Decl α) ℕ} {decl : Std.Sat.AIG.Decl α}
  (h : Std.Sat.AIG.Cache.WF decls cache),
  Std.Sat.AIG.Cache.WF.below h → motive decls cache h → Std.Sat.AIG.Cache.WF.below ⋯
-- Mathlib.Algebra.GroupWithZero.Associated
associated_mul_unit_right : ∀ {N : Type u_2} [inst : Monoid N] (a u : N), IsUnit u → Associated a (a * u)
-- Lean.Data.Lsp.Internal
/-- End character of range.  -/
Lean.Lsp.DeclInfo.rangeEndPosCharacter : Lean.Lsp.DeclInfo → ℕ
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.lratCheckerSound : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : DecidableEq α]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
  [inst_3 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
      ∀ (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
        (∀ a ∈ prf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
          Std.Tactic.BVDecide.LRAT.Internal.lratChecker f prf = Std.Tactic.BVDecide.LRAT.Internal.Result.success →
            Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- The surjective image of a principal ideal ring is again a principal ideal ring.  -/
IsPrincipalIdealRing.of_surjective : ∀ {R : Type u} {S : Type u_1} {F : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [RingHomClass F R S] [IsPrincipalIdealRing R] (f : F), Function.Surjective ⇑f → IsPrincipalIdealRing S
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) (n : ℕ) {Z : ModuleCat k} (h : groupHomology.cycles C n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupHomology.cyclesMap (g.comp f) (CategoryTheory.CategoryStruct.comp φ (Rep.resMap f ψ)) n) h =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ n)
      (CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap g ψ n) h)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The counit of the chosen right Kan extension `rightKanExtension L F`.  -/
CategoryTheory.Functor.rightKanExtensionCounit : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasRightKanExtension F] → L.comp (L.rightKanExtension F) ⟶ F
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The `rw` discrimination tree root.  -/
Mathlib.Tactic.ClickSuggestions.PreDiscrTrees.rw : Mathlib.Tactic.ClickSuggestions.PreDiscrTrees →
  Lean.Meta.RefinedDiscrTree.PreDiscrTree Mathlib.Tactic.ClickSuggestions.RwLemma
-- Lean.Util.PtrSet
Lean.Ptr.mk.inj : ∀ {α : Type u} {value value_1 : α}, { value := value } = { value := value_1 } → value = value_1
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Input.hasNext : {ι : Type} →
  {elem idx : outParam Type} →
    {inst : DecidableEq idx} → {inst_1 : DecidableEq elem} → [self : Std.Internal.Parsec.Input ι elem idx] → ι → Bool
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : C ⥤ₑ D} (α : F ⟶ G), (CategoryTheory.ExactFunctor.forget C D).map α = α.hom
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.σ_injective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), Function.Injective P.σ
-- Mathlib.Topology.LocallyConstant.Basic
/-- The equivalence between `LocallyConstant X Z` and `LocallyConstant Y Z` given a
homeomorphism `X ≃ₜ Y`
 -/
LocallyConstant.congrLeft : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → LocallyConstant X Z ≃ LocallyConstant Y Z
-- Batteries.Data.UInt
UInt64.min_def : ∀ (x y : UInt64), x ⊓ y = if x ≤ y then x else y
-- Mathlib.CategoryTheory.Center.Localization
CategoryTheory.CatCenter.localization_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (r s : CategoryTheory.CatCenter C) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_2 : L.IsLocalization W] [inst_3 : CategoryTheory.Preadditive C] [inst_4 : CategoryTheory.Preadditive D]
  [L.Additive], (r + s).localization L W = r.localization L W + s.localization L W
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_eq_zero_of_lt : ∀ {n p : ℕ}, n < p → n.factorization p = 0
-- Init.Data.List.Range
/-- Replace `zipIdx` with a starting index with `zipIdx` starting from 0,
followed by a `map` increasing the indices.  -/
List.zipIdx_eq_map_add : ∀ {α : Type u_1} {l : List α} {i : ℕ},
  l.zipIdx i =
    List.map
      (fun x =>
        match x with
        | (a, j) => (a, i + j))
      l.zipIdx
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_eq_zero_iff' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι} [NeZero 2]
  [IsDomain R], P.pairing i j = 0 ↔ P.pairing j i = 0
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_iff_ne_singleton : ∀ {α : Type u} {a : α} {s : Set α}, a ∈ s → (s.Nontrivial ↔ s ≠ {a})
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.isQuotientMap_zsmul : ∀ {α : Type u_2} [inst : TopologicalSpace α] {M : Type u_4} {β : Type u_5} [inst_1 : Ring M] [inst_2 : AddCommGroup α]
  [inst_3 : Module M α] [ContinuousConstSMul M α] [inst_5 : AddGroup β] (f : α →+ β) [inst_6 : TopologicalSpace β],
  Topology.IsQuotientMap ⇑f → ∀ (n : ℤ), IsUnit ↑n → Topology.IsQuotientMap fun x => n • x
-- Mathlib.Computability.ContextFreeGrammar
/-- Output string a.k.a. right-hand side.  -/
ContextFreeRule.output : {T : Type u_1} → {N : Type u_2} → ContextFreeRule T N → List (Symbol T N)
-- Init.Data.SInt.Bitwise
Int8.not_inj : ∀ {a b : Int8}, ~~~a = ~~~b ↔ a = b
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.ofNat_ctorIdx : ∀ (x : Lean.Elab.WF.GuessLex.GuessLexRel), Lean.Elab.WF.GuessLex.GuessLexRel.ofNat x.ctorIdx = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.hasPushout_of_left_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.IsIso f],
  CategoryTheory.Limits.HasPushout f g
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : CommSemigroup α], Lex.instCommSemigroup = { toSemigroup := Lex.instSemigroup, mul_comm := ⋯ }
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- No special treatment needed.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.ParentKind.regular : Lean.Meta.Grind.NormalizePattern.ParentKind✝
-- Std.Http.Protocol.H1.Error
/-- The number of header fields in the message exceeds the configured limit.
Maps to HTTP 431 Request Header Fields Too Large.
 -/
Std.Http.Protocol.H1.Error.tooManyHeaders : Std.Http.Protocol.H1.Error
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β k}, a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The canonical linear homeomorphism between `EuclideanSpace 𝕜 (Fin (n + m))` and
`EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m)`.  -/
EuclideanSpace.finAddEquivProd : {𝕜 : Type u_7} →
  [inst : RCLike 𝕜] →
    {n m : ℕ} → EuclideanSpace 𝕜 (Fin (n + m)) ≃L[𝕜] EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.Ref.location : {α : Sort u_1} → Lean.Doc.Ref✝ α → Lean.Syntax
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.Basis.card_le_card_of_submodule : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  {ι' : Type w'} [StrongRankCondition R] (N : Submodule R M) [inst_4 : Fintype ι] (b : Module.Basis ι R M)
  [inst_5 : Fintype ι'] (b' : Module.Basis ι' R ↥N), Fintype.card ι' ≤ Fintype.card ι
-- Mathlib.LinearAlgebra.Matrix.Rank
/-- The rank of a matrix is the rank of its image.  -/
Matrix.rank : {m : Type um} → {n : Type un} → {R : Type uR} → [Fintype n] → [CommSemiring R] → Matrix m n R → ℕ
-- Mathlib.RingTheory.Norm.Transitivity
/-- The main result in Silvester's paper *Determinants of Block Matrices*: the determinant of
a block matrix with commuting, equal-sized, square blocks can be computed by taking determinants
twice in a row: first take the determinant over the commutative ring generated by the
blocks (`S` here), then take the determinant over the base ring.  -/
Matrix.det_det : ∀ {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  (M : Matrix m m S) [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] [inst_4 : Fintype m] [inst_5 : Fintype n]
  (f : S →+* Matrix n n R), (f M.det).det = ((Matrix.comp m m n n R) (M.map ⇑f)).det
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_zero : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R], ⌊0⌋ = 0
-- Mathlib.Tactic.Algebraize
/-- Function that extracts the name of the corresponding `Algebra` property from a `RingHom`
property that has been tagged with the `algebraize` attribute. This is done by either returning the
parameter of the attribute, or by assuming that the tagged declaration has name `RingHom.Property`
and then returning `Algebra.Property`.  -/
Lean.Attr.algebraizeGetParam : Lean.Name → Lean.Syntax → Lean.AttrM Lean.Name