mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.NatInt
/-- `nsmul` is equal to any other module structure via a cast.  -/
ofNat_smul_eq_nsmul : ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
  [inst_3 : n.AtLeastTwo] (b : M), OfNat.ofNat n • b = OfNat.ofNat n • b
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_injective : ∀ {M : Type u_2} [inst : MulOneClass M], Function.Injective Submonoid.unop
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_right' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp (a + p) b = toIocMod hp a b + p
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α)
  (r : ℚ), ↑(hf.stieltjesFunction a) ↑r = f a r
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `smul_apply`. -/
ModularForm.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.false_of_from_star : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  (f : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.of X), False
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.congr_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} {f g : X ⟶ Y}, f = g → F.map f = F.map g
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux.match_1.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (k m : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (m : ℕ) → motive 0 m.succ)
  (h_3 : (k m : ℕ) → motive k.succ m),
  (m = 0 → False) →
    (match k.succ, m with
      | x, 0 => h_1 x
      | 0, m.succ => h_2 m
      | k.succ, m => h_3 k m) =
      h_3 k m
-- Mathlib.RingTheory.Smooth.Basic
/-- For a formally smooth `R`-algebra `A` and a map `f : A →ₐ[R] B ⧸ I` with `I` nilpotent,
this is an arbitrary lift `A →ₐ[R] B`.  -/
Algebra.FormallySmooth.liftOfSurjective : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {B : Type u_1} →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra R B] →
                {C : Type u_4} →
                  [inst_5 : CommRing C] →
                    [inst_6 : Algebra R C] →
                      [Algebra.FormallySmooth R A] →
                        (A →ₐ[R] C) →
                          (g : B →ₐ[R] C) → Function.Surjective ⇑g → IsNilpotent (RingHom.ker ↑g) → A →ₐ[R] B
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inf_eq_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊓ t = s ∩ t
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompAffineEquiv_symm_apply : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : AddTorsor W Q]
  [inst_13 : TopologicalSpace Q] [inst_14 : IsTopologicalAddGroup W] [inst_15 : IsTopologicalAddTorsor Q]
  (p : Q × (V →L[R] W)) (x : V), ((ContinuousAffineMap.decompAffineEquiv R S V Q).symm p) x = p.2 x +ᵥ p.1
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given rings `A, B` and localization maps to their fraction rings
`f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces a semilinear equivalence
fraction rings `K ≃ₛₗ[f.toRingHom] L`.  -/
IsFractionRing.semilinearEquivOfRingEquiv : {A : Type u_8} →
  {B : Type u_9} →
    (K : Type u_10) →
      (L : Type u_11) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : CommRing K] →
              [inst_3 : CommRing L] →
                [inst_4 : Algebra A K] →
                  [IsFractionRing A K] → [inst_6 : Algebra B L] → [IsFractionRing B L] → (f : A ≃+* B) → K ≃ₛₗ[↑f] L
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapAlgebra_mapAlgebra : ∀ {R : Type u} [inst : CommSemiring R] {A : Type u_5} {B : Type u_6} [inst_1 : CommSemiring A] [inst_2 : CommSemiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] {M : CommRing.Pic R},
  (CommRing.Pic.mapAlgebra A B) ((CommRing.Pic.mapAlgebra R A) M) = (CommRing.Pic.mapAlgebra R B) M
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `DivInvMonoid` if it admits an injective map
that preserves `1`, `*`, `⁻¹`, and `/` to a `DivInvMonoid`. See note [reducible non-instances].  -/
Function.Injective.divInvMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : Inv M₁] →
            [inst_4 : Div M₁] →
              [inst_5 : Pow M₁ ℤ] →
                [inst_6 : DivInvMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → DivInvMonoid M₁
-- Lean.Elab.Match
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult.mk : Array Lean.Elab.Term.Discr →
  Lean.Expr → Bool → Array Lean.Elab.Term.TermMatchAltView → Lean.Elab.Term.ElabMatchTypeAndDiscrsResult
-- Mathlib.Topology.Algebra.Support
hasCompactSupport_iff_eventuallyEq : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β},
  HasCompactSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 0
-- Init.Data.SInt.Lemmas
Int8.le_trans : ∀ {a b c : Int8}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.lt_congr : ∀ {α : Type u_1} [inst : LT α] {a b c d : α}, a = b → b < c → d = c → a < d
-- Mathlib.Analysis.Complex.Exponential
/-- The complex exponential function, defined via its Taylor series  -/
Complex.exp : ℂ → ℂ
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mem_toPrepartition : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I}, J ∈ π.toPrepartition ↔ J ∈ π
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- Given `x ∈ s` and a semiring extension `𝕜 ⊆ 𝕜'`, the tangent cone of `s` at `x` with
respect to `𝕜` is contained in the tangent cone of `s` at `x` with respect to `𝕜'`.
 -/
tangentConeAt_mono_field : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x : E} {𝕜' : Type u_3} [inst_3 : Monoid 𝕜'] [inst_4 : SMul 𝕜 𝕜'] [inst_5 : MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E],
  tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x
-- Mathlib.Topology.Connected.PathConnected
pathComponent_congr : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ∈ pathComponent y → pathComponent x = pathComponent y
-- Aesop.Builder.Basic
Aesop.PhaseSpec.unsafe.inj : ∀ {info info_1 : Aesop.UnsafeRuleInfo}, Aesop.PhaseSpec.unsafe info = Aesop.PhaseSpec.unsafe info_1 → info = info_1
-- Mathlib.Order.SuccPred.Basic
/-- See also `Order.le_succ_of_wcovBy`.  -/
Order.succ_eq_of_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α}, a ⋖ b → Order.succ a = b
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.proj.sizeOf_spec : ∀ (typeName : Lean.Name) (idx nargs : ℕ),
  sizeOf (Lean.Meta.RefinedDiscrTree.Key.proj typeName idx nargs) = 1 + sizeOf typeName + sizeOf idx + sizeOf nargs
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.termX : Lean.ParserDescr
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP_eq_splitOnPPrepend : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, List.splitOnP p xs = List.splitOnPPrepend p xs []
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.subtypePerm_apply_zpow_of_mem : ∀ {α : Type u_2} {g : Equiv.Perm α} {s : Finset α} (hs : ∀ (x : α), g x ∈ s ↔ x ∈ s) {i : ℤ} {x : α} (hx : x ∈ s),
  ↑((g.subtypePerm hs ^ i) ⟨x, hx⟩) = (g ^ i) x
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.measure_map_restrict_apply : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  (μ : MeasureTheory.Measure α) (s : Set α) {U : Set (Quotient (MulAction.orbitRel G α))},
  MeasurableSet U →
    (MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (μ.restrict s)) U =
      μ (Quotient.mk (MulAction.orbitRel G α) ⁻¹' U ∩ s)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- **Alias** of the reverse direction of `totallyBounded_absConvexHull`. -/
TotallyBounded.absConvexHull : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : UniformSpace E]
  [IsUniformAddGroup E] [lcs : LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E],
  TotallyBounded s → TotallyBounded ((absConvexHull ℝ) s)
-- Mathlib.Algebra.Ring.Defs
/-- **Alias** of `mul_sub_left_distrib`. -/
mul_sub : ∀ {α : Type u} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * c
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
addLECancellable_add : ∀ {α : Type u_1} [inst : LE α] [inst_1 : AddCommSemigroup α] [AddLeftMono α] {a b : α},
  AddLECancellable (a + b) ↔ AddLECancellable a ∧ AddLECancellable b
-- Lean.Data.FuzzyMatching
/-- Heuristic to penalize skipping characters in the word.  -/
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore.skipPenalty : Lean.FuzzyMatching.CharRole → Bool → Int16
-- Mathlib.Order.ModularLattice
/-- **Alias** of `covBy_sup_of_inf_covBy_left`. -/
CovBy.sup_of_inf_left : ∀ {α : Type u_1} [inst : Lattice α] [IsUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → b ⋖ a ⊔ b
-- Mathlib.Topology.Perfect
perfectSpace_def : ∀ (α : Type u_1) [inst : TopologicalSpace α], PerfectSpace α ↔ Preperfect Set.univ
-- Mathlib.Data.Set.Sups
Set.image_inf_prod : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t : Set α), Set.image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.FullSubcategory.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (obj obj_1 : C)
  (e_obj : obj = obj_1) (property : P obj), { obj := obj, property := property } = { obj := obj_1, property := ⋯ }
-- Mathlib.Data.Vector.Snoc
/-- Define `C v` by *reverse* induction on `v : Vector α n`.
That is, break the vector down starting from the right-most element, using `snoc`

This function has two arguments: `nil` handles the base case on `C nil`,
and `snoc` defines the inductive step using `∀ x : α, C xs → C (xs.snoc x)`.

This can be used as `induction v using Vector.revInductionOn`.  -/
List.Vector.revInductionOn : {α : Type u_1} →
  {C : {n : ℕ} → List.Vector α n → Sort u_5} →
    {n : ℕ} →
      (v : List.Vector α n) →
        C List.Vector.nil → ({n : ℕ} → (xs : List.Vector α n) → (x : α) → C xs → C (xs.snoc x)) → C v
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_bot : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], ↑⊥ = {0}
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.iSup_eq_closure : ∀ {M : Type u_1} [inst : Mul M] {ι : Sort u_3} (p : ι → Subsemigroup M), ⨆ i, p i = Subsemigroup.closure (⋃ i, ↑(p i))
-- Batteries.CodeAction.Misc
/-- The "Remove tactics after 'no goals'" code action deletes any tactics following a completed
proof.
```
example : True := by
  trivial
  trivial -- <- remove this, proof is already done
  rfl
```
is transformed to
```
example : True := by
  trivial
```
 -/
Batteries.CodeAction.removeAfterDoneAction : Batteries.CodeAction.TacticCodeAction
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (a b n : ℤ),
  ((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.stableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsProper
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.ae_measure_preimage_add_right_lt_top_of_ne_zero : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant], ν' s ≠ 0 → ν' s ≠ ⊤ → ∀ᵐ (x : G) ∂μ', ν' ((fun y => y + x) ⁻¹' s) < ⊤
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.subsingleton_of_subsingleton : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [Subsingleton A], Subsingleton (NonUnitalSubalgebra R A)
-- Mathlib.Topology.Algebra.Support
mulTSupport_eq_empty_iff : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] {f : X → α}, mulTSupport f = ∅ ↔ f = 1
-- Init.Internal.Order.Basic
Lean.Order.instCCPOStateRefT' : {m : Type → Type} → {ω σ α : Type} → [inst : Lean.Order.CCPO (m α)] → Lean.Order.CCPO (StateRefT' ω σ m α)
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_multiset_of_nonempty : ∀ (α : Type u) [Nonempty α], Cardinal.mk (Multiset α) = max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasFiniteLimits_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.HasFiniteLimits Cᵒᵖ
-- Mathlib.GroupTheory.Submonoid.Center
Subsemigroup.centerCongr.eq_1 : ∀ {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N),
  Subsemigroup.centerCongr e =
    { toFun := fun r => ⟨e ↑r, ⋯⟩, invFun := fun s => ⟨e.symm ↑s, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Init.Data.UInt.Bitwise
USize.toUInt64_xor : ∀ (a b : USize), (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_support : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → u ≠ 0 → v ≠ 0 → w ≠ 0 → (Polynomial.trinomial k m n u v w).support = {k, m, n}
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.ConvolutionExistsAt.eq_1 : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : Monoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F]
  (L : E →ₗ[S] E' →ₗ[S] F) (f : M → E) (g : M → E') (x : M),
  DiscreteConvolution.ConvolutionExistsAt L f g x = Summable fun ab => (L (f (↑ab).1)) (g (↑ab).2)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.pow_smul_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F : I.Filtration M) (i j : ℕ), I ^ i • F.N j ≤ F.N (i + j)
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_eq_ofInt : ∀ {n : ℤ} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt), Int32.ofIntLE n h₁ h₂ = Int32.ofInt n
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- Evaluation of good products.  -/
Profinite.NobelingProof.GoodProducts.eval : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] → { l // Profinite.NobelingProof.Products.isGood C l } → LocallyConstant ↑C ℤ
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.ofArray.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (l : Array ((a : α) × β a)),
  Std.DHashMap.Raw.ofArray l = ∅.insertMany l
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.mem_support_append_iff : ∀ {V : Type u} {G : SimpleGraph V} {t u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedScheme : Inhabited Std.Http.URI.Scheme
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.ConfigWithKey.mk.inj : ∀ {config : Lean.Meta.Config} {key : UInt64} {config_1 : Lean.Meta.Config} {key_1 : UInt64},
  { config := config, key := key } = { config := config_1, key := key_1 } → config = config_1 ∧ key = key_1
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul : ∀ {M : Type u_1} [inst : Mul M] {a b c D e f : M}, a = b → b = c → c = D * e → e = f → a = D * f
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.bdd_at_cusps' : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (self : ModularForm Γ k) {c : OnePoint ℝ},
  IsCusp c Γ → c.IsBoundedAt self.toFun k
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_X_sub_C : ∀ {R : Type u} [inst : Ring R] (x : R), (Polynomial.X - Polynomial.C x).Monic
-- Init.Data.Order.Classes
/-- If both `a` and `b` satisfy some property `P`, then so does `min a b`, because it is equal to
either `a` or `b`.
 -/
Std.MinEqOr.elim : ∀ {α : Type u} [inst : Min α] [Std.MinEqOr α] {P : α → Prop} {a b : α}, P a → P b → P (a ⊓ b)
-- Batteries.Recycling.RBTree.Basic
/-- Fold a function on the values from left to right (in increasing order).  -/
RBTree.RBNode.Stream.foldl : {σ : Sort u_1} → {α : Type u_2} → (σ → α → σ) → σ → RBTree.RBNode.Stream α → σ
-- Mathlib.RingTheory.Algebraic.Basic
Transcendental.ringHom_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B] [inst_9 : RingHomClass FAB A B]
  (f : FRS) (g : FAB) {a : A},
  Transcendental R a →
    Function.Surjective ⇑f →
      Function.Injective ⇑g → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → Transcendental S (g a)
-- Mathlib.Analysis.Convex.Radon
/-- **Helly's theorem** for families of compact convex sets in its classical form.

If `F` is a (possibly infinite) family of more than `d + 1` compact convex sets in a vector space of
finite dimension `d`, and any `d + 1` sets of `F` intersect nontrivially,
then all sets of `F` intersect nontrivially.  -/
Convex.helly_theorem_compact : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] [inst_6 : TopologicalSpace E] [T2Space E]
  {F : ι → Set E},
  ↑(Module.finrank 𝕜 E) + 1 ≤ ENat.card ι →
    (∀ (i : ι), Convex 𝕜 (F i)) →
      (∀ (i : ι), IsCompact (F i)) →
        (∀ (I : Finset ι), I.card = Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → (⋂ i, F i).Nonempty
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit!_list_of_not_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k k' : α},
      compare k k' = Ordering.eq →
        k ∉ t →
          List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
            k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey? k' = some k
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator_one_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α), ∫⁻ (a : α), s.indicator 1 a ∂μ ≤ μ s
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
/-- Forget being quasi-compact.  -/
AlgebraicGeometry.Scheme.Cover.forgetQc : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.propQCPrecoverage P) S →
      AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The map `p : P ⟶ image f` is an epimorphism  -/
CategoryTheory.Abelian.instEpiFactorThruImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  CategoryTheory.Epi (CategoryTheory.Abelian.factorThruImage f)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.braiding_hom_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C), (X.braiding Y).hom.f = (X.snd.β Y.fst).hom
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) →
      Group ↑(Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteGrp.{max u v} Profinite))).pt.toTop
-- Mathlib.Order.Filter.CardinalInter
/-- A set is in the `cardinalInterFilter` generated by `g` if and only if
it contains an intersection of `c` elements of `g`.  -/
Filter.mem_cardinalGenerate_iff : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {s : Set α} {hreg : c.IsRegular},
  s ∈ Filter.cardinalGenerate g ⋯ ↔ ∃ S ⊆ g, Cardinal.mk ↑S < c ∧ ⋂₀ S ⊆ s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_cons : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) {w : V}
  (h : G.Adj w u),
  SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)
-- Mathlib.Order.GameAdd
/-- `Prod.GameAdd` is a subrelation of `Prod.Lex`.  -/
Prod.gameAdd_le_lex : ∀ {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop), Prod.GameAdd rα rβ ≤ Prod.Lex rα rβ
-- Mathlib.Tactic.Monotonicity.Attr
/-- A lemma stating the monotonicity of some function, with respect to appropriate relations on its
domain and range, and possibly with side conditions.  -/
Mathlib.Tactic.Monotonicity.Attr.mono : Lean.ParserDescr
-- Std.Sync.CancellationToken
Std.CancellationReason.deadline.sizeOf_spec : sizeOf Std.CancellationReason.deadline = 1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.sum_disj_union_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} {M : Type u_2} [inst : AddCommMonoid M],
  Disjoint π₁.iUnion π₂.iUnion →
    ∀ (f : BoxIntegral.Box ι → M), ∑ J ∈ π₁.boxes ∪ π₂.boxes, f J = ∑ J ∈ π₁.boxes, f J + ∑ J ∈ π₂.boxes, f J
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : Cᵒᵖ} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoOpPushout f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f.unop g.unop).op h
-- Lean.Elab.Match
/-- Save pattern information in the info tree, and remove `patternWithRef?` annotations.
 -/
Lean.Elab.Term.ToDepElimPattern.savePatternInfo : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Data.Finset.Sups
Finset.mem_diffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α} {c : α},
  c ∈ s.diffs t ↔ ∃ a ∈ s, ∃ b ∈ t, a \ b = c