mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.insert.eq_1 : ∀ (k : ℤ) (v : Int.Internal.Linear.Var) (k_1 : ℤ),
  Int.Internal.Linear.Poly.insert k v (Int.Internal.Linear.Poly.num k_1) =
    Int.Internal.Linear.Poly.add k v (Int.Internal.Linear.Poly.num k_1)
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type t}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C)
  [inst_4 : CategoryTheory.Limits.HasColimit F] {i j : J} (x : CategoryTheory.ToType (F.obj i))
  (y : CategoryTheory.ToType (F.obj j)),
  (∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) y) →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) y
-- Mathlib.Order.CompleteLattice.Basic
iSup_sup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α},
  (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a
-- Mathlib.Combinatorics.Matroid.Sum
/-- The sum of an indexed collection of matroids on `α` with pairwise disjoint ground sets,
as a matroid on `α`  -/
Matroid.disjointSigma : {α : Type u_1} → {ι : Type u_2} → (M : ι → Matroid α) → Pairwise (Function.onFun Disjoint fun i => (M i).E) → Matroid α
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withTopCongr_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (e : α ≃o β),
  ⇑e.withTopCongr = WithTop.map ⇑e
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral value of a polynomial in `R[X]`, where `R` is a seminormed ring. One motivation
for the spectral value: if the norm on `R` is nonarchimedean, and if a monic polynomial
splits into linear factors, then its spectral value is the norm of its largest root.
See `max_norm_root_eq_spectralValue`.  -/
spectralValue : {R : Type u_1} → [inst : SeminormedRing R] → Polynomial R → ℝ
-- Mathlib.Tactic.DefEqTransformations
/-- Finds all occurrences of expressions of the form `S.mk x.1 ... x.n` where `S.mk`
is a structure constructor and replaces them by `x`.  -/
Mathlib.Tactic.etaStructAll : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.ι_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  {Z : C} (Δ : SimplexCategoryᵒᵖ)
  (F : (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) → s.N (Opposite.unop A.fst).len ⟶ Z)
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (s.desc Δ F) = F A
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.mk.sizeOf_spec : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (ringInst semiringInst : Lean.Expr) (charInst? : Option (Lean.Expr × ℕ))
  (addFn? mulFn? subFn? negFn? powFn? intCastFn? natCastFn? one? : Option Lean.Expr) (vars : Lean.PArray Lean.Expr)
  (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var)
  (denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr),
  sizeOf
      { id := id, type := type, u := u, ringInst := ringInst, semiringInst := semiringInst, charInst? := charInst?,
        addFn? := addFn?, mulFn? := mulFn?, subFn? := subFn?, negFn? := negFn?, powFn? := powFn?,
        intCastFn? := intCastFn?, natCastFn? := natCastFn?, one? := one?, vars := vars, varMap := varMap,
        denote := denote } =
    1 + sizeOf id + sizeOf type + sizeOf u + sizeOf ringInst + sizeOf semiringInst + sizeOf charInst? + sizeOf addFn? +
                        sizeOf mulFn? +
                      sizeOf subFn? +
                    sizeOf negFn? +
                  sizeOf powFn? +
                sizeOf intCastFn? +
              sizeOf natCastFn? +
            sizeOf one? +
          sizeOf vars +
        sizeOf varMap +
      sizeOf denote
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.IsPrimitive.mul_map_mem_lifts_iff : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R] [IsGCDMonoid R] {f : Polynomial R},
  f.IsPrimitive →
    ∀ {g : Polynomial K},
      g * Polynomial.map (algebraMap R K) f ∈ Polynomial.lifts (algebraMap R K) ↔ g ∈ Polynomial.lifts (algebraMap R K)
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousAt.sub` -/
ContinuousAt.fun_sub : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun i => f i - g i) x
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.map.eq_1 : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N),
  AddUnits.map f = AddMonoidHom.mk' (fun u => { val := f ↑u, neg := f u.neg, val_neg := ⋯, neg_val := ⋯ }) ⋯
-- Mathlib.Computability.Ackermann
ack_add_one_sq_lt_ack_add_four : ∀ (m n : ℕ), ack m ((n + 1) ^ 2) < ack (m + 4) n
-- Mathlib.NumberTheory.Real.Irrational
irrational_intCast_sub_iff : ∀ {m : ℤ} {x : ℝ}, Irrational (↑m - x) ↔ Irrational x
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_eq_re_sub_im : ∀ {K : Type u_1} [inst : RCLike K] (z : K), (starRingEnd K) z = ↑(RCLike.re z) - ↑(RCLike.im z) * RCLike.I
-- Mathlib.RepresentationTheory.Induced
Rep.instIsLeftAdjointIndFunctor : ∀ {k : Type u} {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H),
  (Rep.indFunctor k φ).IsLeftAdjoint
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation.compatible_with_triangulation : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.HasShift C ℤ}
  {inst_2 : CategoryTheory.Preadditive C} {inst_3 : CategoryTheory.Limits.HasZeroObject C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {W : CategoryTheory.MorphismProperty C} [self : W.IsCompatibleWithTriangulation]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
  T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
        W a →
          W b →
            CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
              ∃ c,
                ∃ (_ : W c),
                  CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
                    CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map a) =
                      CategoryTheory.CategoryStruct.comp c T₂.mor₃
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.ne_zero_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R}, p ≠ 0 ↔ ∃ d, MvPolynomial.coeff d p ≠ 0
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedMonoid.toMulRightMono : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α], MulRightMono α
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.sub_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Sub γ] [inst_4 : ContinuousSub γ] (f g : C(β, γ)) (h : C(α, β)),
  (f - g).comp h = f.comp h - g.comp h
-- Init.Prelude
Monad.toBind : {m : Type u → Type v} → [self : Monad m] → Bind m
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- Subsingletons are (trivial) blocks.  -/
AddAction.IsBlock.of_subsingleton : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X}, B.Subsingleton → AddAction.IsBlock G B
-- Mathlib.Order.Filter.Partial
Filter.ptendsto_of_ptendsto' : ∀ {α : Type u} {β : Type v} {f : α →. β} {l₁ : Filter α} {l₂ : Filter β},
  Filter.PTendsto' f l₁ l₂ → Filter.PTendsto f l₁ l₂
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_le_size_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, m.size ≤ (m.insert k v).size
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₄_app_three : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ : f.obj' 0 _proof_361✝ ⟶ g.obj' 0 _proof_361✝) (app₁ : f.obj' 1 _proof_362✝ ⟶ g.obj' 1 _proof_362✝)
  (app₂ : f.obj' 2 _proof_363✝ ⟶ g.obj' 2 _proof_363✝) (app₃ : f.obj' 3 _proof_364✝ ⟶ g.obj' 3 _proof_364✝)
  (app₄ : f.obj' 4 _proof_365✝ ⟶ g.obj' 4 _proof_365✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
      _auto_396✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_363✝))
      _auto_398✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_364✝))
      _auto_400✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_365✝))
      _auto_402✝),
  (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app
      ⟨3, CategoryTheory.ComposableArrows.homMk₄._proof_4⟩ =
    app₃
-- Mathlib.CategoryTheory.Shift.Quotient
/-- the condition that the relation is preserved by the shift  -/
HomRel.IsCompatibleWithShift.condition : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {r : HomRel C} {A : Type w} {inst_1 : AddMonoid A}
  {inst_2 : CategoryTheory.HasShift C A} [self : r.IsCompatibleWithShift A] (a : A) ⦃X Y : C⦄ (f g : X ⟶ Y),
  r f g → r ((CategoryTheory.shiftFunctor C a).map f) ((CategoryTheory.shiftFunctor C a).map g)
-- Batteries.Data.DList.Lemmas
Batteries.DList.ofList_toList : ∀ {α : Type u_1} (l : Batteries.DList α), Batteries.DList.ofList l.toList = l
-- Mathlib.Tactic.Ring.RingNF
/-- How to behave if no progress is made: warn, error or keep silent. Default to error  -/
Mathlib.Tactic.RingNF.Config.ifUnchanged : Mathlib.Tactic.RingNF.Config → Mathlib.Tactic.BehaviorIfUnchanged
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x y : α),
  ⇑e ⁻¹' Set.Ioo (e x) (e y) = Set.Ioo x y
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C)
  (t : CategoryTheory.Limits.Cofan f) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I),
  ((CategoryTheory.Limits.FormalCoproduct.isColimitCofan 𝒜 f).desc t).φ p = (t.inj p.fst).φ p.snd
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.proj_pi : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : AddTorsor V1 P1]
  [inst_3 : Module k V1] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11}
  [inst_4 : (i : ι) → AddCommGroup (φv i)] [inst_5 : (i : ι) → Module k (φv i)]
  [inst_6 : (i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (i : ι),
  (AffineMap.proj i).comp (AffineMap.pi fp) = fp i
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (a : α), m.get? a = m_1.get? a
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.d_comp_XIsoOfEq_inv_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι}
  (h : p₃ = p₂) (p₁ : ι) {Z : V} (h_1 : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv h_1) =
    CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h_1
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for morphisms `F ⟶ G` in `ComposableArrows C n` which takes as inputs
a family of morphisms `F.obj i ⟶ G.obj i` and the naturality condition only for the
maps in `Fin (n + 1)` given by inequalities of the form `i ≤ i + 1`.  -/
CategoryTheory.ComposableArrows.homMk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      {F G : CategoryTheory.ComposableArrows C n} →
        (app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i) →
          (∀ (i : ℕ) (hi : i < n),
              CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩) =
                CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩) (G.map' i (i + 1) ⋯ hi)) →
            (F ⟶ G)
-- Mathlib.Topology.MetricSpace.Bounded
/-- The **Heine–Borel theorem**: In a proper space, a closed bounded set is compact.  -/
Metric.isCompact_of_isClosed_isBounded : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] [ProperSpace α],
  IsClosed s → Bornology.IsBounded s → IsCompact s
-- Mathlib.MeasureTheory.Measure.SubFinite
MeasureTheory.Measure.withDensity_sub : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal}
  [MeasureTheory.IsFiniteMeasure (μ.withDensity g)],
  Measurable f → Measurable g → μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanIso_id : ∀ {α : Type u_2} [inst : CommMonoid α] {A : Set α} {n : ℕ}, IsMulFreimanIso n A A id
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
/-- This is the "Lemma" in [mitchell1981].  -/
CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C},
  CategoryTheory.IsSeparator G →
    ∀ {A B : C} {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ} (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)),
      CategoryTheory.Mono g →
        ∀ (f : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ B)),
          CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.kernel.ι (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g))
              (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d f) =
            0
-- Mathlib.Algebra.Order.Group.Defs
exists_zero_lt : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α], ∃ a, 0 < a
-- Mathlib.LinearAlgebra.Basis.Flag
/-- Range of `Basis.flag` as a `Flag`.  -/
Module.Basis.toFlag : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → {n : ℕ} → Module.Basis (Fin n) K V → Flag (Submodule K V)
-- Lean.Meta.WHNF
Lean.Meta.reducePow : Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
BoundedContinuousFunction.innerProbChar_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E],
  BoundedContinuousFunction.innerProbChar 0 = 1
-- Init.Grind.AC
Lean.Grind.AC.Seq.union_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instModule : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → Module A (ρ.IntertwiningMap σ)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_sub : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (m : M) (r s : R),
  AddMonoidAlgebra.single m (r - s) = AddMonoidAlgebra.single m r - AddMonoidAlgebra.single m s
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.inv_zetaUnit : ∀ {R : Type u_1} [inst : CommRing R], ↑ArithmeticFunction.zetaUnit⁻¹ = ↑ArithmeticFunction.moebius
-- Mathlib.Order.Interval.Set.Nat
Set.ncard_uIcc_nat : ∀ (a b : ℕ), (Set.uIcc a b).ncard = (↑b - ↑a).natAbs + 1
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.fst : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {n : ℕ},
  IsMulFreimanHom n (A ×ˢ B) A Prod.fst
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
rootsOfUnity.mkOfPowEq.congr_simp : ∀ {M : Type u_1} [inst : CommMonoid M] (ζ ζ_1 : M) (e_ζ : ζ = ζ_1) {n : ℕ} [inst_1 : NeZero n] (h : ζ ^ n = 1),
  rootsOfUnity.mkOfPowEq ζ h = rootsOfUnity.mkOfPowEq ζ_1 ⋯
-- Mathlib.Computability.Partrec
Computable.option_getD : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → Option β} {g : α → β},
  Computable f → Computable g → Computable fun a => (f a).getD (g a)
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.rTensorOne'_tmul_one : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Submodule R S}
  (m : ↥M), M.rTensorOne' (m ⊗ₜ[R] 1) = m
-- Init.Data.SInt.Lemmas
Int16.toBitVec_toInt32 : ∀ (x : Int16), x.toInt32.toBitVec = BitVec.signExtend 32 x.toBitVec
-- Init.Data.SInt.Lemmas
Int16.lt_or_le : ∀ (a b : Int16), a < b ∨ b ≤ a
-- Init.Data.List.Nat.TakeDrop
List.reverse_drop : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (List.drop i l).reverse = List.take (l.length - i) l.reverse
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.pi_div_two_ne_zero : ↑(Real.pi / 2) ≠ 0
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- A list of transvections such that multiplying on the right with these transvections will replace
the last row with zeroes.  -/
Matrix.Pivot.listTransvecRow : {𝕜 : Type u_3} →
  [Field 𝕜] → {r : ℕ} → Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 → List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem!_set!_ne : ∀ (data : ByteArray) (i j : ℕ) (v : UInt8), i ≠ j → (data.set! i v)[j]! = data[j]!
-- Init.Data.Fin.Basic
Fin.instAdd : {n : ℕ} → Add (Fin n)
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.beckEqualizer_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra)
  (s : CategoryTheory.Limits.Fork (T.map X.a) (T.δ.app X.A)),
  (CategoryTheory.Comonad.beckEqualizer X).lift s = CategoryTheory.CategoryStruct.comp s.ι (T.ε.app X.A)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The kernel of `quotQuotMk`  -/
DoubleQuot.ker_quotQuotMk : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R), RingHom.ker (DoubleQuot.quotQuotMk I J) = I ⊔ J
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.support_derivativeFinsupp_subset_range : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ},
  p.natDegree < n → (Polynomial.derivativeFinsupp p).support ⊆ Finset.range n
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame.title : Lean.VersoModuleDocs.DocFrame✝ → Array (Lean.Doc.Inline Lean.ElabInline)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_refl_iff : ∀ {α : Type u_1} {f : Equiv.Perm α}, f.Disjoint f ↔ f = 1
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_Ici_succ : ∀ {n : ℕ} (i : Fin n), Fin.succ ⁻¹' Set.Ici i.succ = Set.Ici i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : Nontrivial R}
  {inst_2 : StarRing R} {inst_3 : MetricSpace R} {inst_4 : IsTopologicalSemiring R} {inst_5 : ContinuousStar R}
  {inst_6 : NonUnitalRing A} {inst_7 : StarRing A} {inst_8 : MetricSpace A} {inst_9 : Module R A}
  {inst_10 : IsScalarTower R A A} {inst_11 : SMulCommClass R A A}
  [self : NonUnitalIsometricContinuousFunctionalCalculus R A p], NonUnitalContinuousFunctionalCalculus R A p
-- Mathlib.Topology.Algebra.Group.Basic
/-- If a subgroup of an additive topological group is commutative, then so is its
topological closure.

See note [reducible non-instances].  -/
AddSubgroup.addCommGroupTopologicalClosure : {G : Type w} →
  [inst : TopologicalSpace G] →
    [inst_1 : AddGroup G] →
      [inst_2 : IsTopologicalAddGroup G] →
        [T2Space G] → (s : AddSubgroup G) → (∀ (x y : ↥s), x + y = y + x) → AddCommGroup ↥s.topologicalClosure
-- Init.Grind.ToInt
/-- The embedding takes `OfNat` to `OfNat`.  -/
Lean.Grind.ToInt.OfNat.toInt_ofNat : ∀ {α : Type u} {inst : (n : ℕ) → OfNat α n} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.OfNat α I] (n : ℕ), ↑(OfNat.ofNat n) = I.wrap ↑n
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `LinearMap.rTensor`  -/
TensorProduct.AlgebraTensorModule.rTensor : (R : Type uR) →
  {A : Type uA} →
    {M : Type uM} →
      (N : Type uN) →
        {P : Type uP} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : Algebra R A] →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module A M] →
                      [inst_6 : IsScalarTower R A M] →
                        [inst_7 : AddCommMonoid N] →
                          [inst_8 : Module R N] →
                            [inst_9 : AddCommMonoid P] →
                              [inst_10 : Module R P] →
                                [inst_11 : Module A P] →
                                  [inst_12 : IsScalarTower R A P] →
                                    (M →ₗ[A] P) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R P N
-- Mathlib.Algebra.Order.Hom.Basic
map_inv_mul : ∀ {F : Type u_2} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : PartialOrder β] (f : F) {α : Type u_7}
  [inst_2 : FunLike F α β] [inst_3 : CommGroup α] [GroupSeminormClass F α β] (x y : α), f (x⁻¹ * y) = f (x * y⁻¹)
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_asymm` -/
ssubset_asymm : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → ¬b ⊂ a
-- Std.Data.ExtHashSet.Basic
/-- Removes all elements from the hash set for which the given function returns `false`.  -/
Std.ExtHashSet.filter : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → (α → Bool) → Std.ExtHashSet α → Std.ExtHashSet α
-- Mathlib.GroupTheory.Finiteness
AddGroup.closure_finite_fg : ∀ {G : Type u_3} [inst : AddGroup G] (s : Set G) [Finite ↑s], AddGroup.FG ↥(AddSubgroup.closure s)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.distortion_biUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Fintype ι] (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J),
  (π.biUnion πi).distortion = π.boxes.sup fun J => (πi J).distortion
-- Mathlib.Topology.Algebra.ConstMulAction
continuousOn_const_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G]
  [inst_2 : AddAction G α] [ContinuousConstVAdd G α] [inst_4 : TopologicalSpace β] {f : β → α} {s : Set β} (c : G),
  ContinuousOn (fun x => c +ᵥ f x) s ↔ ContinuousOn f s
-- Std.Net.Addr
/-- Representation of a MAC address.
 -/
Std.Net.MACAddr : Type