mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Linear.Basic
/-- Composition by a fixed left argument as an `R`-linear map.  -/
CategoryTheory.Linear.leftComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (R : Type w) →
        [inst_2 : Semiring R] →
          [inst_3 : CategoryTheory.Linear R C] → {X Y : C} → (Z : C) → (X ⟶ Y) → (Y ⟶ Z) →ₗ[R] X ⟶ Z
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.symm.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (cme : M ≃ₜ+ N), cme.symm = { toAddEquiv := cme.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.instIsCoverDenseEtaleSpecSmallEtaleTopology : ∀ {S : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.AffineEtale.Spec S).IsCoverDense S.smallEtaleTopology
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.PropSetWithTop`.

---

Given `J : CardinalFilteredPoset κ` and a regular cardinal `κ'`,
this is the predicate on `Set J.withTop.obj` that is satisfied by
subsets that are of cardinality `< κ'` and contain `⊤`.  -/
CategoryTheory.CardinalFilteredPoset.PropSetWithTop : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) → (κ' : Cardinal.{u}) → [Fact κ'.IsRegular] → Set ↑J.withTop.obj → Prop
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_subtype_true : ∀ {α : Type u_1}, Nat.card { _a // True } = Nat.card α
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : CategoryTheory.Monad C} {c c' : CategoryTheory.Kleisli T}
  [inst_1 : SizeOf C] (of : c.of ⟶ T.obj c'.of), sizeOf { of := of } = 1 + sizeOf of
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instWeakEquivalenceP₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.weakEquivalences C).ContainsIdentities], HomotopicalAlgebra.WeakEquivalence P.p₁
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Tendsto.atTop_nsmul_neg_const : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [inst : AddCommGroup R] [inst_1 : LinearOrder R]
  [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℕ},
  r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x • r) l Filter.atBot
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.mem_restrictDegree_iff_sup : ∀ (σ : Type u) {R : Type v} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p : MvPolynomial σ R) (n : ℕ),
  p ∈ MvPolynomial.restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i p.degrees ≤ n
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- The degree of `f` equals to the degree of `leadingTerm f`  -/
MonomialOrder.degree_leadingTerm : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.degree (m.leadingTerm f) = m.degree f
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- There exists `π : R` with `v`-adic valuation `WithZero.exp (-1)`.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  ∃ π, (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑π = WithZero.exp (-1)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (i : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt.I),
  (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd.φ i = (pb i).snd
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.tail_support_perm_dropLast_support : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u), p.support.tail.Perm p.support.dropLast
-- Mathlib.Data.Nat.Log
Nat.log.go.match_1.congr_eq_1 : ∀ (motive : ℕ × ℕ → Sort u_1) (x : ℕ × ℕ) (h_1 : (q e : ℕ) → motive (q, e)) (q e : ℕ),
  x = (q, e) →
    (match x with
      | (q, e) => h_1 q e) ≍
      h_1 q e
-- Mathlib.Algebra.Quandle
/-- The dihedral quandle. This is the conjugation quandle of the dihedral group restricted to flips.

Used for Fox n-colorings of knots.  -/
Quandle.Dihedral : ℕ → Type
-- Init.Data.List.Lex
List.instAsymmLt : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2], Std.Asymm fun x1 x2 => x1 < x2
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.differentiableWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f₀ f₁ : E → F} {x : E} {s : Set E},
  f₀ =ᶠ[nhdsWithin x s] f₁ → f₀ x = f₁ x → (DifferentiableWithinAt 𝕜 f₀ s x ↔ DifferentiableWithinAt 𝕜 f₁ s x)
-- Mathlib.Algebra.Lie.Nilpotent
/-- If a Lie module `M` contains a self-normalizing Lie submodule `N`, then all terms of the upper
central series of `M` are contained in `N`.

An important instance of this situation arises from a Cartan subalgebra `H ⊆ L` with the roles of
`L`, `M`, `N` played by `H`, `L`, `H`, respectively.  -/
LieSubmodule.ucs_le_of_normalizer_eq_self : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] {N₁ : LieSubmodule R L M}
  [inst_6 : LieModule R L M], N₁.normalizer = N₁ → ∀ (k : ℕ), LieSubmodule.ucs k ⊥ ≤ N₁
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.Equicontinuous.continuous_of_mem : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H : Set (X → α)},
  H.Equicontinuous → ∀ {f : X → α}, f ∈ H → Continuous f
-- Init.SizeOf
Lean.ParserDescr.parser.sizeOf_spec : ∀ (declName : Lean.Name), sizeOf (Lean.ParserDescr.parser declName) = 1 + sizeOf declName
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Generators.ker_localizationAway : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S],
  (Algebra.Generators.localizationAway S r).ker = Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1}
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.liftₐ_comp_toAlgHom : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal A) [inst_5 : I.IsPrime] (f : A →ₐ[R] B)
  (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B)),
  (Ideal.ResidueField.liftₐ I f hf₁ hf₂).comp (IsScalarTower.toAlgHom R A I.ResidueField) = f
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftAlgHom_apply_div' : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} {S : Type u_3} [inst_2 : Field L]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S (Polynomial K)] [inst_5 : Algebra S L] (φ : Polynomial K →ₐ[S] L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K),
  (RatFunc.liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) /
      (RatFunc.liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) =
    φ p / φ q
-- Mathlib.Probability.Process.HittingTime
/-- This lemma is strictly weaker than `hittingBtwn_of_le`.  -/
MeasureTheory.hittingBtwn_of_lt : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} {m : ι}, m < n → MeasureTheory.hittingBtwn u s n m ω = m
-- Mathlib.Order.Atoms
IsCoatom.codisjoint_of_ne : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α},
  IsCoatom a → IsCoatom b → a ≠ b → Codisjoint a b
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
polarCoord_source_ae_eq_univ : polarCoord.source =ᵐ[MeasureTheory.volume] Set.univ
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.dual : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  t.Bounded o₁ o₂ → t.dual.Bounded o₂ o₁
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_eval₂_mul_of_commute : ∀ {S : Type u_2} {A : Type u_3} [inst : Semiring S] [inst_1 : Semiring A] {p : Polynomial S} (f : S →+* A) (a : A)
  (s : S),
  Commute (f s) a →
    (∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)) →
      Polynomial.eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree * Polynomial.eval₂ f a p
-- Init.Data.Option.Basic
Option.bind_some : ∀ {α : Type u_1} {β : Type u_2} (a : α) (f : α → Option β), (some a).bind f = f a
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_X_sub_C : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R),
  m.Monic (MvPolynomial.X i - MvPolynomial.C r)
-- Mathlib.Order.Filter.Lift
Filter.lift'_id : ∀ {α : Type u_1} {f : Filter α}, f.lift' id = f
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_getThenInsertIfNew? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(m.getThenInsertIfNew? a b).2
-- Mathlib.Algebra.Order.Star.Basic
/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
show that the nonnegative elements are precisely those elements in the `AddSubmonoid` generated
by `star s * s` for `s : R`.  -/
StarOrderedRing.of_nonneg_iff : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R],
  (∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y) →
    (∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)) → StarOrderedRing R
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selfLeftAction_actionAssocIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x y z =
    CategoryTheory.MonoidalCategoryStruct.associator x y z
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj₂.isIdempotent_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [Std.IdempotentOp ga],
  Function.Semiconj₂ f ga gb → Function.Surjective f → Std.IdempotentOp gb
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.eq_div_of_subst : ∀ {M : Type u_1} [inst : Div M] {l l_n l_d n d : M}, l = l_n / l_d → l_n = n → l_d = d → l = n / d
-- Mathlib.Tactic.CongrM
/-- `congrm e` is a tactic for proving goals of the form `lhs = rhs`, `lhs ↔ rhs`, `lhs ≍ rhs`,
or `R lhs rhs` when `R` is a reflexive relation.
The expression `e` is a pattern containing placeholders `?_`,
and this pattern is matched against `lhs` and `rhs` simultaneously.
These placeholders generate new goals that state that corresponding subexpressions
in `lhs` and `rhs` are equal.
If the placeholders have names, such as `?m`, then the new goals are given tags with those names.

Examples:
```lean
example {a b c d : ℕ} :
    Nat.pred a.succ * (d + (c + a.pred)) = Nat.pred b.succ * (b + (c + d.pred)) := by
  congrm Nat.pred (Nat.succ ?h1) * (?h2 + ?h3)
  /-  Goals left:
  case h1 ⊢ a = b
  case h2 ⊢ d = b
  case h3 ⊢ c + a.pred = c + d.pred
  -/
  sorry
  sorry
  sorry

example {a b : ℕ} (h : a = b) : (fun y : ℕ => ∀ z, a + a = z) = (fun x => ∀ z, b + a = z) := by
  congrm fun x => ∀ w, ?_ + a = w
  -- ⊢ a = b
  exact h
```

The `congrm` command is a convenient frontend to `congr(...)` congruence quotations.
If the goal is an equality, `congrm e` is equivalent to `refine congr(e')` where `e'` is
built from `e` by replacing each placeholder `?m` by `$(?m)`.
The pattern `e` is allowed to contain `$(...)` expressions to immediately substitute
equality proofs into the congruence, just like for congruence quotations.
 -/
Mathlib.Tactic.congrM : Lean.ParserDescr
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderRetractsMonoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.monoModSerre.IsStableUnderRetracts
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.containsThenInsert_fst : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.containsThenInsert k v).1 = m.contains k
-- Mathlib.GroupTheory.Finiteness
/-- The product of two finitely generated additive groups is finitely generated.  -/
Prod.instAddGroupFG : ∀ {G : Type u_3} [inst : AddGroup G] {G' : Type u_5} [inst_1 : AddGroup G'] [AddGroup.FG G] [AddGroup.FG G'],
  AddGroup.FG (G × G')
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.insertMany_array_eq_insertMany_toList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (a : Array ((k : α) × β k)), m.insertMany a = m.insertMany a.toList
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.cocone_naturality : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (F.map f) (RingCat.Colimits.coconeMorphism F j') =
    RingCat.Colimits.coconeMorphism F j
-- Mathlib.LinearAlgebra.Basis.SMul
/-- Given a basis `v` and a map `w` such that for all `i`, `w i` is a unit, `unitsSMul`
provides the basis corresponding to `w • v`.  -/
Module.Basis.unitsSMul : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module.Basis ι R M → (ι → Rˣ) → Module.Basis ι R M
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isGE₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C),
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n : ℤ), t.IsGE T.obj₁ n → t.IsGE T.obj₃ n → t.IsGE T.obj₂ n
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.mk : {σ : Type} →
  ℕ →
    IO σ →
      (Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit) →
        (Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit) →
          (Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit) →
            Lean.Meta.Grind.GoalM Bool →
              Lean.Meta.Grind.Action →
                Lean.Meta.Grind.GoalM Bool → Lean.Meta.Grind.GoalM Unit → Lean.Meta.Grind.SolverExtension σ
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.shrink : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Small.{w, v} M]
  [Module.IsStablyFree R M], Module.IsStablyFree R (Shrink.{w, v} M)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instNonemptyMapEmbedding : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Nonempty] {f : α ↪ β}, (M.mapEmbedding f).Nonempty
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.Pairing.instNonemptyWeakRankFunctionNat : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsRegular], Nonempty (P.WeakRankFunction ℕ)
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_map_iff : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} {f : β → α},
  Cauchy (Filter.map f l) ↔ l.NeBot ∧ Filter.Tendsto (fun p => (f p.1, f p.2)) (l ×ˢ l) (uniformity α)
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitForall.finalize : Array Lean.Expr →
  Array Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Data.UInt
UInt64.toBitVec_natCast : ∀ (n : ℕ), (↑n).toBitVec = ↑n
-- Mathlib.Order.Filter.Basic
Filter.frequently_and_distrib_right : ∀ {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop}, (∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_of_nsmul : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ), (n • FreeAddGroup.of a).toWord = List.replicate n (a, true)
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
dvd_smul_of_dvd : ∀ {R : Type u_1} {M : Type u_2} [inst : SMul M R] [inst_1 : Semigroup R] [SMulCommClass M R R] {x y : R} (m : M),
  x ∣ y → x ∣ m • y
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnosticsParams.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {version : ℕ} {uri_1 : Lean.Lsp.DocumentUri} {version_1 : ℕ},
  { uri := uri, version := version } = { uri := uri_1, version := version_1 } → uri = uri_1 ∧ version = version_1
-- Mathlib.Data.ZMod.Units
ZMod.unitsMap_self : ∀ (n : ℕ), ZMod.unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ
-- Init.Data.Array.OfFn
Array.ofFnM_succ : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α},
  Array.ofFnM f = do
    let as ← Array.ofFnM fun i => f i.castSucc
    let a ← f (Fin.last n)
    pure (as.push a)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.algHomClass : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B], AlgHomClass (A →ₐ[R] B) R A B
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
bitvector literal.
 -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.fromExpr? : Lean.Expr → Lean.Meta.SimpM (Option BitVec.Literal✝)
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_indicator : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] (T : Set α → F →L[ℝ] F'),
  T ∅ = 0 →
    ∀ {m : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) (x : F),
      MeasureTheory.SimpleFunc.setToSimpleFunc T
          (MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α x)
            (MeasureTheory.SimpleFunc.const α 0)) =
        (T s) x
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofNat_im : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ) [inst_1 : n.AtLeastTwo], RCLike.im (OfNat.ofNat n) = 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C),
  (t.triangleLEGE a b h).obj X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.elabSimpConfig : Lean.Syntax → Lean.Elab.Tactic.SimpKind → Lean.Elab.Tactic.TacticM Lean.Meta.Simp.ConfigWithOptions
-- Init.Data.List.Count
List.count_le_count_map : ∀ {α : Type u_2} [inst : BEq α] [LawfulBEq α] {β : Type u_1} [inst_2 : BEq β] [LawfulBEq β] {l : List α} {f : α → β}
  {x : α}, List.count x l ≤ List.count (f x) (List.map f l)
-- Lean.Elab.Do.Basic
/-- Prepare the context for elaborating the body of a loop.
This includes setting the return continuation, break continuation, continue continuation, as
well as the changed result type of the `do` block in the loop body.
 -/
Lean.Elab.Do.enterLoopBody : {α : Type} →
  Lean.Elab.Do.DoElabM Lean.Expr →
    Lean.Elab.Do.DoElabM Lean.Expr → Lean.Elab.Do.ReturnCont → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toTopologicalSpace_top : ∀ {α : Type u} [inst : AddGroup α], ⊤.toTopologicalSpace = ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_congr : ∀ {R : Type u_1} {A : Type u_2} {p : 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 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {f g : R → R} {a : A},
  Set.EqOn f g (quasispectrum R a) → cfcₙ f a = cfcₙ g a
-- Batteries.Data.Fin.Lemmas
Fin.eq_none_of_findSomeRev?_eq_none : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, Fin.findSomeRev? f = none → ∀ (i : Fin n), f i = none
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.symm_of_of : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  (x : GradedTensorProduct R 𝒜 ℬ), (GradedTensorProduct.of R 𝒜 ℬ) ((GradedTensorProduct.of R 𝒜 ℬ).symm x) = x
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} (aig : Std.Sat.AIG α) (input : aig.BinaryRefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func]
  [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α func],
  aig.decls.size ≤ (Std.Sat.AIG.RefVec.zip aig input func).aig.decls.size
-- Mathlib.MeasureTheory.Group.Measure
/-- A nonzero left-invariant regular measure gives positive mass to any open set.  -/
MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] [NeZero μ], μ.IsOpenPosMeasure
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) {X Y : P.I} (f : X ⟶ Y),
  (P.toCostructuredArrow.map f).left = P.F.map f
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_injective_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂}, Function.Injective ⇑f → Function.Injective (Submodule.map f)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumComm_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'], ⇑(Diffeomorph.sumComm I M n M') = Sum.swap