mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Util.Profile
/-- Print and accumulate run time of `act` when option `profiler` is set to `true`.  -/
Lean.profileit : {α : Type} → String → Lean.Options → (Unit → α) → optParam Lean.Name Lean.Name.anonymous → α
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instIsRightCancelAdd : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Add M] [IsRightCancelAdd M], IsRightCancelAdd (l.Germ M)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.isFixedPt_reflection_of_isOrthogonal : ∀ {ι : 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} {j : ι} {s : Set ι},
  (∀ i ∈ s, P.IsOrthogonal j i) →
    ∀ {x : M}, x ∈ Submodule.span R (⇑P.root '' s) → Function.IsFixedPt (⇑(P.reflection j)) x
-- Mathlib.RingTheory.Unramified.Locus
Algebra.basicOpen_subset_unramifiedLocus_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {f : A},
  ↑(PrimeSpectrum.basicOpen f) ⊆ Algebra.unramifiedLocus R A ↔ Algebra.FormallyUnramified R (Localization.Away f)
-- Aesop.Stats.Extension
Aesop.mkStatsArray : List Aesop.StatsExtensionEntry → Array (Array Aesop.StatsExtensionEntry) → Aesop.StatsArray
-- Lean.DocString.Extension
/-- Saved data that describes a custom inline element.

The type of value contained within the `Dynamic` determines the interpretation of the custom
element, including how it is rendered to Markdown for the language server.
 -/
Lean.ElabInline : Type
-- Mathlib.Order.Category.BoolAlg
BoolAlg.Iso.mk_hom : ∀ {α β : BoolAlg} (e : ↑α ≃o ↑β),
  (BoolAlg.Iso.mk e).hom =
    BoolAlg.ofHom
      (have __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.χ_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G)
  (χ' : G ⟶ CategoryTheory.Functor.sieves C),
  CategoryTheory.IsPullback m
      ((CategoryTheory.Functor.isTerminalConst Cᵒᵖ CategoryTheory.Limits.Types.isTerminalPUnit).from F) χ'
      (CategoryTheory.Presheaf.truth C) →
    χ' = CategoryTheory.Presheaf.χ m
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mem_stabilizer_finset_iff_subset_smul_finset : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} [inst_2 : DecidableEq α]
  {s : Finset α}, a ∈ MulAction.stabilizer G s ↔ s ⊆ a • s
-- Std.Data.Internal.List.Associative
Std.Internal.List.modifyKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f f_1 : β k → β k),
  f = f_1 →
    ∀ (l l_1 : List ((a : α) × β a)),
      l = l_1 → Std.Internal.List.modifyKey k f l = Std.Internal.List.modifyKey k f_1 l_1
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_zero_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (a : R), (MvPowerSeries.coeff 0) (MvPowerSeries.C a) = a
-- Lean.Meta.ArgsPacker
Lean.Meta.ArgsPacker.onlyOneUnary : Lean.Meta.ArgsPacker → Bool
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- The typeclass associated with the structure `EquivalenceRelation`.  -/
CategoryTheory.IsEquivalenceRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R X : C} → (R ⟶ X) → (R ⟶ X) → Prop
-- Std.Time.Format.Modifier
Std.Time.Modifier.e.inj : ∀ {presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text},
  Std.Time.Modifier.e presentation = Std.Time.Modifier.e presentation_1 → presentation = presentation_1
-- Init.Data.SInt.Lemmas
Int8.lt_iff_toInt_lt : ∀ {x y : Int8}, x < y ↔ x.toInt < y.toInt
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.uniqueOfIsEmpty : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → [IsEmpty ι] → Unique (Π₀ (i : ι), β i)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.alterKey.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (k : α) →
      (motive : Option (β k) → Sort u_2) →
        (x : Option (β k)) → (Unit → motive none) → ((v : β k) → motive (some v)) → motive x
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The algebra homomorphism `(A / I) / J' -> A / (I ⊔ J)` induced by `quotQuotToQuotSup`,
where `J'` is the projection of `J` in `A / I`.  -/
DoubleQuot.quotQuotToQuotSupₐ : (R : Type u) →
  {A : Type u_1} →
    [inst : CommSemiring R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] → (I J : Ideal A) → (A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J →ₐ[R] A ⧸ I ⊔ J
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H1InfRes_X₃ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupCohomology.H1InfRes A S).X₃ = groupCohomology (Rep.res S.subtype A) 1
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- A version of `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum`
in terms of the value of the series.  -/
EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  f 1 = 1 →
    (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
      (Summable fun x => ‖f x‖) →
        ∀ (N : ℕ), ∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n) = ∑' (m : ↑N.smoothNumbers), f ↑m
-- Mathlib.Data.EReal.Operations
EReal.sub_self_le_zero : ∀ {x : EReal}, x - x ≤ 0
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.unsat_relabel : ∀ {α : Type u_1} {β : Type u_2} {f : Std.Sat.CNF α} (r : α → β), f.Unsat → (Std.Sat.CNF.relabel r f).Unsat
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_bot : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α}, ↑⊥ = ⊥
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infDist_eq_iInf : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, Metric.infDist x s = ⨅ y, dist x ↑y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is a commutative group object, then `Hom(X, G)` has a commutative group structure.  -/
CategoryTheory.Hom.commGroup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G X : C} →
        [inst_2 : CategoryTheory.GrpObj G] →
          [inst_3 : CategoryTheory.BraidedCategory C] → [CategoryTheory.IsCommMonObj G] → CommGroup (X ⟶ G)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisors.eq_1 : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀], nonZeroDivisors M₀ = nonZeroDivisorsLeft M₀ ⊓ nonZeroDivisorsRight M₀
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.toEquiv_eq_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (f : M ≃ₜ+ N), f.toEquiv = ↑f
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.symm_trans_self : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (e : α ≃+*o β), e.symm.trans e = OrderRingIso.refl β
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.workspaceSymbolProvider : Lean.Lsp.ServerCapabilities → Bool
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_fst_lt_agm_of_pos_of_ne : ∀ {x y : NNReal}, 0 < x → 0 < y → x ≠ y → ∀ (n : ℕ), (x.agmSequences y n).1 < x.agm y
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.matroid_indep_iff : ∀ {α : Type u_1} {M : IndepMatroid α} {I : Set α}, M.matroid.Indep I ↔ M.Indep I
-- Mathlib.Topology.Convenient.GeneratedBy
TopologicalSpace.generatedBy.eq_1 : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y],
  TopologicalSpace.generatedBy X = ⨆ i, ⨆ f, TopologicalSpace.coinduced (⇑f) inferInstance
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.mutuallySingular_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), (μ.singularPart ν).MutuallySingular ν
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
two_mul_natCast_pentagonal_neg : ∀ (k : ℤ), 2 * ↑(pentagonal (-k)) = k * (3 * k + 1)
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.unicodeVariant.injEq : ∀ (s : String) (selector : Option Char) (s_1 : String) (selector_1 : Option Char),
  (Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ s selector =
      Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ s_1 selector_1) =
    (s = s_1 ∧ selector = selector_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A convenient way to show that a binary cofan is a colimit.  -/
CategoryTheory.Limits.BinaryCofan.IsColimit.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (s : CategoryTheory.Limits.BinaryCofan X Y) →
        (desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)) →
          (∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), CategoryTheory.CategoryStruct.comp s.inl (desc f g) = f) →
            (∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), CategoryTheory.CategoryStruct.comp s.inr (desc f g) = g) →
              (∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T),
                  CategoryTheory.CategoryStruct.comp s.inl m = f →
                    CategoryTheory.CategoryStruct.comp s.inr m = g → m = desc f g) →
                CategoryTheory.Limits.IsColimit s
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- **Alias** of the forward direction of `ContinuousLinearMapWOT.continuousOn_iff`. -/
ContinuousLinearMapWOT.continuousOn_inner_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α},
  ContinuousOn f s → ∀ (x : E) (y : F), ContinuousOn (fun x_1 => inner 𝕜 y ((f x_1) x)) s
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_prod : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R] (ι : Type u_2) (s : Finset ι) (f : ι → R),
  (∀ x ∈ s, f x ≠ 0) → Differential.logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, Differential.logDeriv (f x)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instFaithfulMonForget₂Mon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.Grp.forget₂Mon C).Faithful
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.eq_univ_or_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} [WellFoundedGT α], IsUpperSet s → s = Set.univ ∨ ∃ a, s = Set.Ioi a
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_eq_zero_iff : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h → h ∈ Γ.strictPeriods → ∀ {k : ℤ} (f : ModularForm Γ k), UpperHalfPlane.qExpansion h ⇑f = 0 ↔ f = 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocEntry.mk.injEq : ∀ (toSimprocOLeanEntry : Lean.Meta.Simp.SimprocOLeanEntry) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)
  (toSimprocOLeanEntry_1 : Lean.Meta.Simp.SimprocOLeanEntry)
  (proc_1 : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc),
  ({ toSimprocOLeanEntry := toSimprocOLeanEntry, proc := proc } =
      { toSimprocOLeanEntry := toSimprocOLeanEntry_1, proc := proc_1 }) =
    (toSimprocOLeanEntry = toSimprocOLeanEntry_1 ∧ proc = proc_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Unitization.instStarOrderedRing : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A], StarOrderedRing (Unitization ℂ A)
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.instNatPowOfNat : {ι : Type u_1} → (A : ι → Type u_2) → [inst : AddMonoid ι] → [GradedMonoid.GMonoid A] → NatPow (A 0)
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.le.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α},
  Localization.le = { le := fun a b => a.liftOn₂ b (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ ≤ ↑a₂ * b₁) ⋯ }
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) (n : ℤ), logDeriv (fun x => x ^ n) x = ↑n / x
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- The functoriality of `H.obj G` identifies (through
`Wedge.IsLimit.hom_ext`) with the functoriality on ends induced by
functoriality of `internalHomDiagramFunctor F|>.obj G`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (self : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) {c c' : C} (f : c ⟶ c') (j : C) {Z : V}
  (h : F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (H.map f) (CategoryTheory.CategoryStruct.comp (self.π c' j) h) =
    CategoryTheory.CategoryStruct.comp (self.π c j)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f))) h)
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabDoElems.prependAndRec : Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM (List Lean.Syntax)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.instFullCompPre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) [F.Full], (CategoryTheory.CostructuredArrow.pre F G S).Full
-- Std.Data.TreeMap.Basic
/-- Internal implementation detail of the tree map.  -/
Std.TreeMap.inner : {α : Type u} →
  {β : Type v} →
    {cmp : autoParam (α → α → Ordering) Std.TreeMap._auto_1} → Std.TreeMap α β cmp → Std.DTreeMap α (fun x => β) cmp
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_reflectionPerm : ∀ {ι : 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 : ι},
  P.reflection ((P.reflectionPerm j) i) = P.reflection j * P.reflection i * P.reflection j
-- Mathlib.Logic.Function.DependsOn
DependsOn.mono : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} {f : ((i : ι) → α i) → β} {s t : Set ι},
  s ⊆ t → DependsOn f s → DependsOn f t
-- Lean.Meta.TryThis
/-- Pretty-prints a `SuggestionText` as a `Format`. If the `SuggestionText` is some `TSyntax kind`,
we use the appropriate pretty-printer; strings are coerced to `Format`s as-is.  -/
Lean.Meta.Tactic.TryThis.SuggestionText.pretty : Lean.Meta.Tactic.TryThis.SuggestionText → Lean.CoreM Std.Format
-- Mathlib.RingTheory.TensorProduct.Maps
TensorProduct.AlgebraTensorModule.assoc.congr_simp : ∀ (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (P : Type uP) (Q : Type uQ) [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid P] [inst_13 : Module A P] [inst_14 : AddCommMonoid Q] [inst_15 : Module R Q]
  [inst_16 : Module R P] [inst_17 : IsScalarTower R A P] [inst_18 : Algebra A B] [inst_19 : IsScalarTower A B M],
  TensorProduct.AlgebraTensorModule.assoc R A B M P Q = TensorProduct.AlgebraTensorModule.assoc R A B M P Q
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.mapHomologyIso_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hl : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasHomology]
  [inst_6 : (S.map F).HasHomology] [inst_7 : F.PreservesLeftHomologyOf S],
  S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm
-- Mathlib.Algebra.Ring.Basic
AddHom.mulRight_apply : ∀ {R : Type u_1} [inst : Distrib R] (r : R), ⇑(AddHom.mulRight r) = fun a => a * r
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
summable_finsetProd_of_summable_norm : ∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] {f : ι → R} [CompleteSpace R],
  (Summable fun i => ‖f i‖) → Summable fun s => ∏ i ∈ s, f i
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.isPrefix_aig : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α β f]
  (aig : Std.Sat.AIG α) (input : β aig), Std.Sat.AIG.IsPrefix aig.decls (f aig input).aig.decls
-- Mathlib.Data.Set.NAry
Set.image2_inter_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
  Function.Injective2 f → Set.image2 f s (t ∩ t') = Set.image2 f s t ∩ Set.image2 f s t'
-- Lean.Meta.ExprLens
/-- Runs `k` on the given coordinate, including handling binders properly.
The subexpression value passed to `k` is not instantiated with respect to the
array of free variables.  -/
_private.Lean.Meta.ExprLens.0.Lean.Meta.viewCoordAux : {M : Type → Type} →
  [Monad M] →
    [MonadControlT Lean.MetaM M] →
      [Lean.MonadError M] → {α : Type} → (Array Lean.Expr → Lean.Expr → M α) → Array Lean.Expr → ℕ → Lean.Expr → M α
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_roo : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Roo.Sliceable.mkSlice xs lo<...hi).array = xs
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.beq.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  [inst_3 : (k : α) → BEq (β k)] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.beq m₂ = if (↑m₁).size ≠ (↑m₂).size then false else (↑m₁).all fun k v => m₂.get? k == some v
-- Init.Data.Array.Count
Array.filter_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] [inst_2 : DecidableEq α] {xs : Array α} (a : α),
  Array.filter (fun x => decide (x = a)) xs = Array.replicate (Array.count a xs) a
-- Mathlib.Order.Interval.Basic
/-- Turn an interval into an interval in the dual order.  -/
NonemptyInterval.dual : {α : Type u_1} → [inst : LE α] → NonemptyInterval α ≃ NonemptyInterval αᵒᵈ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α},
  m₁.WF → m₂.WF → ∀ (f : α → Bool), m₁.Equiv m₂ → (Std.HashSet.Raw.filter f m₁).Equiv (Std.HashSet.Raw.filter f m₂)
-- Mathlib.Data.Set.Prod
Set.union_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {s₁ s₂ : Set ι} {t : (i : ι) → Set (α i)}, (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCardAux.eq_1 : ∀ {α : Type u_1} (n : ℕ) (l : List α), Multiset.powersetCardAux n l = List.sublistsLenAux n l Multiset.ofList []
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.GAlgebra.commutes : ∀ {ι : Type uι} {R : Type uR} {A : ι → Type uA} {inst : CommSemiring R} {inst_1 : (i : ι) → AddCommMonoid (A i)}
  {inst_2 : (i : ι) → Module R (A i)} {inst_3 : AddMonoid ι} {inst_4 : DirectSum.GSemiring A}
  [self : DirectSum.GAlgebra R A] (r : R) (x : GradedMonoid A),
  GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r) * x = x * GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r)
-- Batteries.Data.List.Basic
/-- Auxiliary for `takeDTR`: `takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt`.  -/
List.takeDTR.go : {α : Type u_1} → α → ℕ → List α → Array α → List α
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.one_of_succ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 (n + 1) f s → ContDiffOn 𝕜 1 f s
-- Mathlib.Algebra.NeZero
four_ne_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], 4 ≠ 0
-- Mathlib.Order.Bounds.Basic
/-- If `a` is a greatest lower bound for sets `s` and `p`, then it is a greater lower
bound for any set `t`, `s ⊆ t ⊆ p`.  -/
IsGLB.of_subset_of_superset : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {s t p : Set α}, IsGLB s a → IsGLB p a → s ⊆ t → t ⊆ p → IsGLB t a
-- Mathlib.Order.Lattice
left_eq_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a = a ⊔ b ↔ b ≤ a
-- Std.Time.Internal.Bounded
/-- Creates a new `Bounded` integer that the relation is less-equal.
 -/
Std.Time.Internal.Bounded.LE.mk : {lo hi : ℤ} → (val : ℤ) → lo ≤ val ∧ val ≤ hi → Std.Time.Internal.Bounded.LE lo hi
-- Mathlib.Order.WithBotTop
/-- The type obtained by adding both `⊥` and `⊤` to a type.  -/
WithBotTop : Type u_1 → Type u_1
-- Init.Coe
boolToSort : CoeSort Bool Prop
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.mk.sizeOf_spec : ∀ (thm : Lean.Meta.Grind.EMatchTheorem) (proof prop : Lean.Expr) (generation : ℕ)
  (guards : List Lean.Meta.Grind.TheoremGuard) (sources : List Lean.Meta.Grind.EMatchDiagNode),
  sizeOf { thm := thm, proof := proof, prop := prop, generation := generation, guards := guards, sources := sources } =
    1 + sizeOf thm + sizeOf proof + sizeOf prop + sizeOf generation + sizeOf guards + sizeOf sources
-- Mathlib.FieldTheory.KummerExtension
autEquivRootsOfUnity.congr_simp : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a a_1 : K} (e_a : a = a_1)
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] [inst_4 : NeZero n],
  autEquivRootsOfUnity hζ H L = autEquivRootsOfUnity hζ ⋯ L
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- If a finset `u` is contained in the scalar product of two sets `s • t`, we can find two finsets
`s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' • t'`.  -/
Finset.subset_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {u : Finset β} {s : Set α} {t : Set β},
  ↑u ⊆ s • t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' • t'
-- Init.Tactics
/-- `apply e` tries to match the current goal against the conclusion of `e`'s type.
If it succeeds, then the tactic returns as many subgoals as the number of premises that
have not been fixed by type inference or type class resolution.
Non-dependent premises are added before dependent ones.

The `apply` tactic uses higher-order pattern matching, type class resolution,
and first-order unification with dependent types.


Extensions:

 * * `apply (config := cfg) e` allows for additional configuration (see `Lean.Meta.ApplyConfig`):
     * `newGoals` controls which new goals are added by `apply`, in which order.
     * `-synthAssignedInstances` will not synthesize instance implicit arguments if they have been
       assigned by `isDefEq`.
     * `+allowSynthFailures` will create new goals when instance synthesis fails, rather than erroring.
     * `+approx` enables `isDefEq` approximations (see `Lean.Meta.approxDefEq`). -/
Lean.Parser.Tactic.apply : Lean.ParserDescr