mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.hasBasis_nhds_zero_of_basis : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F] {ι : Type u_7}
  {p : ι → Prop} {b : ι → Set F},
  (nhds 0).HasBasis p b →
    (nhds 0).HasBasis (fun Si => Bornology.IsVonNBounded 𝕜₁ Si.1 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
-- Mathlib.Algebra.Free
FreeMagma.hom_ext_iff : ∀ {α : Type u} {β : Type v} [inst : Mul β] {f g : FreeMagma α →ₙ* β}, f = g ↔ ⇑f ∘ FreeMagma.of = ⇑g ∘ FreeMagma.of
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.toComplex_ι : ∀ (r : ℝ), CliffordAlgebraComplex.toComplex ((CliffordAlgebra.ι CliffordAlgebraComplex.Q) r) = r • Complex.I
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.EvalTerm.mk : {α : Type} → (Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)) → Lean.Expr → Lean.Elab.ConfigEval.EvalTerm α
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.eqToIso_hom : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ = S₂), (SSet.Subcomplex.eqToIso h).hom = SSet.Subcomplex.homOfLE ⋯
-- Init.Core
DoResultPRBC.break.inj : ∀ {α β σ : Type u} {a a_1 : σ}, DoResultPRBC.break a = DoResultPRBC.break a_1 → a = a_1
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- A tensor product `M ⊗[R] N` is the direct limit of the modules `P ⊗[R] N`,
where `P` ranges over all finitely generated submodules of `M`, as a linear equivalence.  -/
Submodule.FG.rTensor.directLimit : (R : Type u) →
  (M : Type u_1) →
    (N : Type u_2) →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : DecidableEq { P // P.FG }] →
                  (Module.DirectLimit (fun P => TensorProduct R (↥↑P) N) fun ⦃P Q⦄ h =>
                      LinearMap.rTensor N (Submodule.inclusion h)) ≃ₗ[R]
                    TensorProduct R M N
-- Mathlib.Logic.Equiv.Option
Equiv.optionEquivSumPUnit_symm_inl : ∀ {α : Type u_4} (a : α), (Equiv.optionEquivSumPUnit α).symm (Sum.inl a) = some a
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_symm_apply' : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : r₁ ⟶ r₂),
  (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂).symm α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor l₂).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight adj₁.unit l₂)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator l₁ r₁ l₂).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft l₁ (CategoryTheory.Bicategory.whiskerRight α l₂))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft l₁ adj₂.counit)
              (CategoryTheory.Bicategory.rightUnitor l₁).hom))))
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.add_martingale : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Supermartingale f ℱ μ → MeasureTheory.Martingale g ℱ μ → MeasureTheory.Supermartingale (f + g) ℱ μ
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Lp.toTemperedDistributionCLM_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : CompleteSpace F] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
  {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] {p : ENNReal} [hp : Fact (1 ≤ p)]
  (f : ↥(MeasureTheory.Lp F p μ)),
  (MeasureTheory.Lp.toTemperedDistributionCLM F μ p) f = MeasureTheory.Lp.toTemperedDistribution f
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.IndParallelPairPresentation.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B}
  {I : Type v₁} {ℐ : CategoryTheory.SmallCategory I} {hI : CategoryTheory.IsFiltered I}
  {F₁ F₂ : CategoryTheory.Functor I C} {ι₁ : F₁.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A}
  {isColimit₁ : CategoryTheory.Limits.IsColimit { pt := A, ι := ι₁ }}
  {ι₂ : F₂.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj B}
  {isColimit₂ : CategoryTheory.Limits.IsColimit { pt := B, ι := ι₂ }} {φ ψ : F₁ ⟶ F₂}
  {hf : f = isColimit₁.map { pt := B, ι := ι₂ } (CategoryTheory.Functor.whiskerRight φ CategoryTheory.yoneda)}
  {hg : g = isColimit₁.map { pt := B, ι := ι₂ } (CategoryTheory.Functor.whiskerRight ψ CategoryTheory.yoneda)}
  {I_1 : Type v₁} {ℐ_1 : CategoryTheory.SmallCategory I_1} {hI_1 : CategoryTheory.IsFiltered I_1}
  {F₁_1 F₂_1 : CategoryTheory.Functor I_1 C}
  {ι₁_1 : F₁_1.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I_1).obj A}
  {isColimit₁_1 : CategoryTheory.Limits.IsColimit { pt := A, ι := ι₁_1 }}
  {ι₂_1 : F₂_1.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I_1).obj B}
  {isColimit₂_1 : CategoryTheory.Limits.IsColimit { pt := B, ι := ι₂_1 }} {φ_1 ψ_1 : F₁_1 ⟶ F₂_1}
  {hf_1 : f = isColimit₁_1.map { pt := B, ι := ι₂_1 } (CategoryTheory.Functor.whiskerRight φ_1 CategoryTheory.yoneda)}
  {hg_1 : g = isColimit₁_1.map { pt := B, ι := ι₂_1 } (CategoryTheory.Functor.whiskerRight ψ_1 CategoryTheory.yoneda)},
  { I := I, ℐ := ℐ, hI := hI, F₁ := F₁, F₂ := F₂, ι₁ := ι₁, isColimit₁ := isColimit₁, ι₂ := ι₂,
        isColimit₂ := isColimit₂, φ := φ, ψ := ψ, hf := hf, hg := hg } =
      { I := I_1, ℐ := ℐ_1, hI := hI_1, F₁ := F₁_1, F₂ := F₂_1, ι₁ := ι₁_1, isColimit₁ := isColimit₁_1, ι₂ := ι₂_1,
        isColimit₂ := isColimit₂_1, φ := φ_1, ψ := ψ_1, hf := hf_1, hg := hg_1 } →
    I = I_1 ∧
      ℐ ≍ ℐ_1 ∧
        F₁ ≍ F₁_1 ∧
          F₂ ≍ F₂_1 ∧ ι₁ ≍ ι₁_1 ∧ isColimit₁ ≍ isColimit₁_1 ∧ ι₂ ≍ ι₂_1 ∧ isColimit₂ ≍ isColimit₂_1 ∧ φ ≍ φ_1 ∧ ψ ≍ ψ_1
-- Init.Prelude
PProd.mk : {α : Sort u} → {β : Sort v} → α → β → α ×' β
-- Mathlib.Topology.GDelta.Basic
/-- The union of two Gδ sets is a Gδ set.  -/
IsGδ.union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, IsGδ s → IsGδ t → IsGδ (s ∪ t)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isOpen_iff : ∀ {R : Type u} [inst : CommSemiring R] (U : Set (PrimeSpectrum R)), IsOpen U ↔ ∃ s, Uᶜ = PrimeSpectrum.zeroLocus s
-- Init.Data.Nat.Gcd
Nat.div_gcd_pos_of_pos_right : ∀ {b : ℕ} (a : ℕ), 0 < b → 0 < b / a.gcd b
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.add.inj : ∀ {R : Type u_1} {X : Type u_2} {a a_1 a_2 a_3 : FreeAlgebra.Pre R X}, a.add a_1 = a_2.add a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Order.Group.Synonym
isAddRightRegular_toColex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddRightRegular (toColex a) ↔ IsAddRightRegular a
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The type of Dirichlet characters of level `n`.  -/
DirichletCharacter : (R : Type u_1) → [CommMonoidWithZero R] → ℕ → Type (max 0 u_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.maxKey?.isSome = !t.isEmpty
-- Mathlib.MeasureTheory.VectorMeasure.Prod
MeasureTheory.VectorMeasure.HasProd.exists_prod : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} {inst_2 : NormedAddCommGroup F}
  {inst_3 : NormedSpace ℝ F} {inst_4 : NormedAddCommGroup G} {inst_5 : NormedSpace ℝ G}
  {μ : MeasureTheory.VectorMeasure X E} {ν : MeasureTheory.VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G}
  [self : μ.HasProd ν B],
  ∃ ρ, ∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)
-- Mathlib.Data.Finmap
Finmap.lookup.congr_simp : ∀ {α : Type u} {β : α → Type v} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a : α) (s s_1 : Finmap β),
  s = s_1 → Finmap.lookup a s = Finmap.lookup a s_1
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.Hom.ext : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Over Q X} {f g : A ⟶ B}, f.left = g.left → f = g
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.IsMulSpanning.eq_1 : ∀ {G : Type u_1} [inst : Group G] (M : Submonoid G), M.IsMulSpanning = ∀ (a : G), a ∈ M ∨ a⁻¹ ∈ M
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_div_left : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α}, s.Nonempty → t.card ≤ (s / t).card
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_op_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] (s : Finset α),
  Finset.image AddOpposite.op (-s) = -Finset.image AddOpposite.op s
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_forIn : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] {α : Type uu} (as : List α) (init : β)
  (f : γ → α → β → m (ForInStep β)), Lean.Order.monotone f → Lean.Order.monotone fun x => forIn as init (f x)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.PseudoCore.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.LaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a))
  (mapCompIso :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
  (mapIdIso_inv :
    autoParam (∀ {a : B}, (mapIdIso a).inv = F.mapId a) CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv._autoParam)
  (mapCompIso_inv :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).inv = F.mapComp f g)
      CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv._autoParam),
  sizeOf
      { mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_inv := mapIdIso_inv,
        mapCompIso_inv := mapCompIso_inv } =
    1
-- Lean.Data.Lsp.Extra
/-- The pretty-printed goals, empty if all accomplished.  -/
Lean.Lsp.PlainGoal.goals : Lean.Lsp.PlainGoal → Array String
-- Mathlib.RingTheory.Morita.Basic
/-- For any `R`-algebras `A` and `B`, if `A` is Morita equivalent to `B`, then `B` is Morita equivalent
to `A`.
 -/
MoritaEquivalence.symm : (R : Type u₀) →
  [inst : CommSemiring R] →
    {A : Type u₁} →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          {B : Type u₂} → [inst_3 : Ring B] → [inst_4 : Algebra R B] → MoritaEquivalence R A B → MoritaEquivalence R B A
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `AddAction.isBlock_iff_disjoint_vadd_of_ne`. -/
AddAction.IsBlock.disjoint_vadd_of_ne : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B → ∀ ⦃g : G⦄, g +ᵥ B ≠ B → Disjoint (g +ᵥ B) B
-- Mathlib.Data.Vector3
/-- Eliminator for an empty vector.  -/
Vector3.nilElim : {α : Type u_1} → {C : Vector3 α 0 → Sort u} → C [] → (v : Vector3 α 0) → C v
-- Mathlib.GroupTheory.ClassEquation
Group.card_center_add_sum_card_noncenter_eq_card : ∀ (G : Type u_2) [inst : Group G] [inst_1 : (x : ConjClasses G) → Fintype ↑x.carrier] [inst_2 : Fintype G]
  [inst_3 : Fintype ↥(Subgroup.center G)] [inst_4 : Fintype ↑(ConjClasses.noncenter G)],
  Fintype.card ↥(Subgroup.center G) + ∑ x ∈ (ConjClasses.noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.initial_mono_of_strict_initial_objects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C],
  CategoryTheory.Limits.InitialMonoClass C
-- Mathlib.RingTheory.AdjoinRoot
/-- The natural isomorphism `R[α]/I[α] ≅ (R/I)[X]/(f mod I)` for `α` a root of `f : R[X]`
and `I : Ideal R`.  -/
AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (f : Polynomial R) →
        AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.of f) I ≃+*
          Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.mem_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {F : Type u_3}
  [inst_2 : FunLike F R S] (f : F) [inst_3 : NonUnitalRingHomClass F R S] {I : TwoSidedIdeal S} {x : R},
  x ∈ (TwoSidedIdeal.comap f) I ↔ f x ∈ I
-- Mathlib.LinearAlgebra.Multilinear.DirectSum
MultilinearMap.fromDirectSumEquiv_symm_apply : ∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  [inst_5 : DecidableEq ι] [inst_6 : Finite ι] [inst_7 : (i : ι) → DecidableEq (κ i)]
  (f : MultilinearMap R (fun i => DirectSum (κ i) fun j => M i j) M') (p : (i : ι) → κ i),
  MultilinearMap.fromDirectSumEquiv.symm f p = f.compLinearMap fun i => DirectSum.lof R (κ i) (M i) (p i)
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- We say that `P : AffineTargetMorphismProperty` is a local property if
1. `P` respects isomorphisms.
2. If `P` holds for `f : X ⟶ Y`, then `P` holds for `f ∣_ Y.basicOpen r` for any
  global section `r`.
3. If `P` holds for `f ∣_ Y.basicOpen r` for all `r` in a spanning set of the global sections,
  then `P` holds for `f`.
 -/
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal : AlgebraicGeometry.AffineTargetMorphismProperty → Prop
-- Mathlib.Algebra.Order.Hom.Ring
/-- `OrderRingIso α β`, denoted as `α ≃+*o β`,
is the type of order-preserving semiring isomorphisms between `α` and `β`.

When possible, instead of parametrizing results over `(f : OrderRingIso α β)`,
you should parametrize over `(F : Type*) [OrderRingIsoClass F α β] (f : F)`.

When you extend this structure, make sure to extend `OrderRingIsoClass`.  -/
«term_≃+*o_» : Lean.TrailingParserDescr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.eval_const : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {b : Bool},
  Std.Tactic.BVDecide.BVLogicalExpr.eval assign (Std.Tactic.BVDecide.BoolExpr.const b) = b
-- Mathlib.CategoryTheory.ConnectedComponents
/-- This gives that any category is equivalent to a disjoint union of connected categories.  -/
CategoryTheory.decomposedEquiv : {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.Decomposed J ≌ J
-- Mathlib.Analysis.Fourier.Notation
ContinuousFourierInv.continuous_fourierInv : ∀ {E : Type u_5} {F : outParam (Type u_6)} {inst : TopologicalSpace E} {inst_1 : TopologicalSpace F}
  {inst_2 : FourierTransformInv E F} [self : ContinuousFourierInv E F], Continuous FourierTransformInv.fourierInv
-- Init.Grind.Attr
/-- The `←=` modifier is unlike the other `grind` modifiers, and it used specifically for
backwards reasoning on equality. When a theorem's conclusion is an equality proposition and it
is annotated with `@[grind ←=]`, grind `will` instantiate it whenever the corresponding disequality
is assumed—this is a consequence of the fact that grind performs all proofs by contradiction.
Ordinarily, the grind attribute does not consider the `=` symbol when generating patterns.
 -/
Lean.Parser.Attr.grindEqBwd : Lean.ParserDescr
-- Mathlib.Algebra.Module.Injective
/-- An `R`-module `Q` is injective if and only if every injective `R`-linear map descends to a linear
map to `Q`, i.e. in the following diagram, if `f` is injective then there is an `R`-linear map
`h : Y ⟶ Q` such that `g = h ∘ f`
  ```
  X --- f ---> Y
  |
  | g
  v
  Q
  ```
 -/
Module.Injective : (R : Type u) → [inst : Ring R] → (Q : Type v) → [inst_1 : AddCommGroup Q] → [Module R Q] → Prop
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_comp_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (a : 𝕜),
  iteratedDeriv n (fun x => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)
-- Mathlib.Tactic.Cases
/-- `induction' x` applies induction on the variable `x` of the inductive type `t` to the main goal,
producing one goal for each constructor of `t`, in which `x` is replaced by that constructor
applied to newly introduced variables. `induction'` adds an inductive hypothesis for
each recursive argument to the constructor. This is a backwards-compatible variant of the
`induction` tactic in Lean 4 core.

Prefer `induction` when possible, because it promotes structured proofs.

* `induction' x with n1 n2 ...` names the introduced hypotheses: arguments to constructors and
  inductive hypotheses. This is the main difference with `induction` in core Lean.
* `induction' e`, where `e` is an expression instead of a variable, generalizes `e` in the goal,
  and then performs induction on the resulting variable.
* `induction' h : e`, where `e` is an expression instead of a variable, generalizes `e` in the goal,
  and then performs induction on the resulting variable, adding to each goal the hypothesis
  `h : e = _` where `_` is the constructor instance.
* `induction' x using r` uses `r` as the principle of induction. Here `r` should be a term whose
  result type is of the form `C t1 t2 ...`, where `C` is a bound variable and `t1`, `t2`, ... (if
  present) are bound variables.
* `induction' x generalizing z1 z2 ...` generalizes over the local variables `z1`, `z2`, ... in the
  inductive hypothesis.

Example:
```
open Nat

example (n : ℕ) : 0 < factorial n := by
  induction' n with n ih
  · rw [factorial_zero]
    simp
  · rw [factorial_succ]
    apply mul_pos (succ_pos n) ih

-- Though the following equivalent spellings should be preferred
example (n : ℕ) : 0 < factorial n := by
  induction n
  case zero =>
    rw [factorial_zero]
    simp
  case succ n ih =>
    rw [factorial_succ]
    apply mul_pos (succ_pos n) ih
```
 -/
Mathlib.Tactic.induction' : Lean.ParserDescr
-- Mathlib.RingTheory.Morita.Basic
/-- Let `A` and `B` be `R`-algebras. We say that `A` and `B` are Morita equivalent if the categories of
`A`-modules and `B`-modules are equivalent as `R`-linear categories.
 -/
IsMoritaEquivalent : (R : Type u₀) →
  [inst : CommSemiring R] →
    (A : Type u₁) → [inst_1 : Ring A] → [Algebra R A] → (B : Type u₂) → [inst_3 : Ring B] → [Algebra R B] → Prop
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.eqCnstr? : Lean.Expr → Lean.MetaM (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr × Array Lean.Expr))
-- Init.Data.Dyadic.Basic
Rat.lt_toRat_toDyadic_add : ∀ {x : ℚ} {prec : ℤ}, x < (x.toDyadic prec + Dyadic.ofIntWithPrec 1 prec).toRat
-- Mathlib.Algebra.Order.Kleene
kstar_mul_le_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, KStar.kstar a * a ≤ KStar.kstar a
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.instInhabited : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} → Inhabited (Monoid.PushoutI.NormalWord d)
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.insert.match_1.eq_1 : ∀ (motive : List ℕ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (a : ℕ) → (as : List ℕ) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.isNat_gcd : ∀ {x y nx ny z : ℕ},
  Mathlib.Meta.NormNum.IsNat x nx →
    Mathlib.Meta.NormNum.IsNat y ny → nx.gcd ny = z → Mathlib.Meta.NormNum.IsNat (x.gcd y) z
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mem_verts_of_mem_edge : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {e : Sym2 V} {v : V}, e ∈ G'.edgeSet → v ∈ e → v ∈ G'.verts
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.swap_map : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {X Y : B × C}
  (a : X ⟶ Y), (CategoryTheory.Bicategory.Prod.swap B C).map a = CategoryTheory.Prod.mkHom a.2 a.1
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Fractional operation is a fractional polymorphism for given VCSP template.  -/
FractionalOperation.IsFractionalPolymorphismFor : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] → {m : ℕ} → FractionalOperation D m → ValuedCSP D C → Prop
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_map : ∀ {V : Type u_1} [inst : Fintype V] {W : Type u_2} [inst_1 : Fintype W] [inst_2 : DecidableEq W] (f : V ↪ W)
  (G : SimpleGraph V) [inst_3 : DecidableRel G.Adj],
  (SimpleGraph.map (⇑f) G).edgeFinset = Finset.map f.sym2Map G.edgeFinset
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.universally_mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  {X Y : C} (g : X ⟶ Y),
  (∀ {T : C} (f : T ⟶ Y) [inst_2 : CategoryTheory.Limits.HasPullback f g], P (CategoryTheory.Limits.pullback.fst f g)) →
    P.universally g
-- Mathlib.Data.Nat.Prime.Basic
Nat.not_prime_mul : ∀ {a b : ℕ}, a ≠ 1 → b ≠ 1 → ¬Nat.Prime (a * b)
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.forget_map : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (f : A ⟶ B),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (CommBialgCat R)).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.PFun
/-- Image of a set under a partial function.  -/
PFun.image : {α : Type u_1} → {β : Type u_2} → (α →. β) → Set α → Set β
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Init.Data.Int.Bitwise.Lemmas
Int.le_shiftRight_of_nonneg : ∀ {n : ℤ} {s : ℕ}, 0 ≤ n → 0 ≤ n >>> s
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.forget₂_map : ∀ (R : Type u) [inst : Ring R] (X Y : ModuleCat R) (f : X ⟶ Y),
  (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map f = AddCommGrpCat.ofHom ↑(ModuleCat.Hom.hom f)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.constantsOnMap_inclusion_isExpansionOn : ∀ {M : Type w} {A B : Set M} (h : A ⊆ B), (FirstOrder.Language.LHom.constantsOnMap (Set.inclusion h)).IsExpansionOn M
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.Lean.MVarId.userCongr?.forSide : Congr!.Config → Lean.MVarId → Lean.Expr → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjOpcyclesSelfIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((HomologicalComplex.single C c j).map f) j)
      (HomologicalComplex.singleObjOpcyclesSelfIso c j B).inv =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv f