mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Modular
/-- Classify cases when `z ∈ 𝒟` and `g • z ∈ 𝒟` such that `c = 0`.  -/
_private.Mathlib.NumberTheory.Modular.0.ModularGroup.cases_c_zero : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd →
    g • z ∈ ModularGroup.fd →
      ↑g 1 0 = 0 →
        (g = ModularGroup.T ∨ g = -ModularGroup.T) ∧ z.re = -1 / 2 ∨
          (g = ModularGroup.T⁻¹ ∨ g = -ModularGroup.T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.coe_star : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Subalgebra R A), ↑(star S) = star ↑S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β},
  t.Equiv Std.DTreeMap.Internal.Impl.empty ↔ t.isEmpty = true
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.homModule : {R : Type w} →
  {inst : Semiring R} →
    {C : Type u} →
      {inst_1 : CategoryTheory.Category.{v, u} C} →
        {inst_2 : CategoryTheory.Preadditive C} → [self : CategoryTheory.Linear R C] → (X Y : C) → Module R (X ⟶ Y)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.int.injEq : ∀ (i i_1 : ℤ), (Aesop.Frontend.Priority.int i = Aesop.Frontend.Priority.int i_1) = (i = i_1)
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.instIsMulCommutative_closure : ∀ (M : Type u_1) [inst : Semigroup M] {S : Type u_2} [inst_1 : SetLike S M] [inst_2 : MulMemClass S M] (s : S)
  [IsMulCommutative ↥s], IsMulCommutative ↥(Subsemigroup.closure ↑s)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_toHomeomorph : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ⇑e.toHomeomorph = ⇑e
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.coe_id : ∀ (A : Type u_1) [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A], ⇑(NonUnitalStarRingHom.id A) = id
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.ideal_isMaximal_iff : ∀ {X : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [CompactSpace X] [T2Space X]
  (I : Ideal C(X, 𝕜)) [hI : IsClosed ↑I], I.IsMaximal ↔ ∃ x, ContinuousMap.idealOfSet 𝕜 {x}ᶜ = I
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.hom_ext'_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} {hf' : F.relativelyRepresentable f'} {a : C}
  {g : F.obj a ⟶ Y} [inst_2 : F.Full] [F.Faithful] {c : C} {a_1 b_1 : c ⟶ hf'.pullback g},
  a_1 = b_1 ↔
    CategoryTheory.CategoryStruct.comp a_1 (hf'.fst' g) = CategoryTheory.CategoryStruct.comp b_1 (hf'.fst' g) ∧
      CategoryTheory.CategoryStruct.comp a_1 (hf'.snd g) = CategoryTheory.CategoryStruct.comp b_1 (hf'.snd g)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- **Alias** of the reverse direction of `ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff`.

---

`range f` is invariant under `T` if and only if `f ∘L T ∘L f = T ∘L f`,
for idempotent `f`.  -/
ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f T : M →L[R] M},
  IsIdempotentElem f → f ∘SL T ∘SL f = T ∘SL f → (↑f).range ∈ Module.End.invtSubmodule ↑T
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.UniversallyClosed f ↔ (AlgebraicGeometry.topologically @IsClosedMap).universally f
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The underlying type of `WalkingIso` is equivalent to `Bool`, since they both have 2 elements.  -/
CategoryTheory.WalkingIso.equivBool : CategoryTheory.WalkingIso ≃ Bool
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.trans_isLittleO : ∀ {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : Norm β₂] {l : Filter α}
  {f g₁ : α → β} {g₂ : α → β₂}, Asymptotics.IsEquivalent l f g₁ → g₁ =o[l] g₂ → f =o[l] g₂
-- Mathlib.RingTheory.PowerSeries.Restricted
/-- Restricted power series as an subring of `PowerSeries R`.  -/
PowerSeries.IsRestricted.subring : {R : Type u_1} → [inst : NormedRing R] → [IsUltrametricDist R] → ℝ → Subring (PowerSeries R)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eq_some_getEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α}
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getEntry? a l = some (Std.Internal.List.getEntry a l h)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.ContentLength.mk : ℕ → Std.Http.Header.ContentLength
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instAddCommGroup : {σ : Type u_1} → {R : Type u_2} → [AddCommGroup R] → AddCommGroup (MvPowerSeries σ R)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.motive.injEq : ∀ (decl : Lean.LocalDecl) (motiveIdx : ℕ) (vars : Array Lean.FVarId) (decl_1 : Lean.LocalDecl) (motiveIdx_1 : ℕ)
  (vars_1 : Array Lean.FVarId),
  (Lean.Meta.IndPredBelow.NewDecl.motive✝ decl motiveIdx vars =
      Lean.Meta.IndPredBelow.NewDecl.motive✝ decl_1 motiveIdx_1 vars_1) =
    (decl = decl_1 ∧ motiveIdx = motiveIdx_1 ∧ vars = vars_1)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- `liftToFinset`, when composed with the evaluation functor, results in the whiskering composed
with `colim`.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetEvaluationIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        (I : Finset (CategoryTheory.Discrete α)) →
          (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).comp
              ((CategoryTheory.evaluation (Finset (CategoryTheory.Discrete α)) C).obj I) ≅
            ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete ↥I) (CategoryTheory.Discrete α) C).obj
                  (CategoryTheory.Discrete.functor fun x => ↑x)).comp
              CategoryTheory.Limits.colim
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.toFinsuppAntidiag.eq_1 : ∀ {n : ℕ} (p : n.Partition),
  p.toFinsuppAntidiag =
    { support := p.parts.toFinset, toFun := fun m => Multiset.count m p.parts * m, mem_support_toFun := ⋯ }
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.SubobjectRepresentableBy.iso_inv_hom_left_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m] {Z : C}
  (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (h.iso m).inv.hom)
      (CategoryTheory.CategoryStruct.comp m h_1) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Subobject.pullback (h.χ m)).obj h.Ω₀).arrow h_1
-- Mathlib.Data.PFun
PFun.coe : {α : Type u_1} → {β : Type u_2} → Coe (α → β) (α →. β)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insertIfNew k v).maxKey?.isSome = true
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_eq_foldl : ∀ {α : Type u} {x : Ord α} {l : List α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} (h : t.Balanced),
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l h) =
    List.foldl (fun acc k => Std.DTreeMap.Internal.Impl.insertIfNew! k () acc) t l
-- Mathlib.Algebra.Ring.Periodic
Finset.periodic_sum : ∀ {α : Type u_1} {β : Type u_2} {c : α} [inst : Add α] [inst_1 : AddCommMonoid β] {ι : Type u_4} {f : ι → α → β}
  (s : Finset ι), (∀ i ∈ s, Function.Periodic (f i) c) → Function.Periodic (∑ i ∈ s, f i) c
-- Mathlib.Data.Erased
/-- Computably produce an erased value from a proof of nonemptiness.  -/
Erased.choice : {α : Sort u_1} → Nonempty α → Erased α
-- Lean.Elab.Do.Basic
Lean.Elab.Do.SavedState.mk.sizeOf_spec : ∀ (term : Lean.Elab.Term.SavedState), sizeOf { term := term } = 1 + sizeOf term
-- Init.Data.Array.Zip
Array.zipWith_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as : Array α} {bs : Array β},
  Array.zipWith f as bs = #[] ↔ as = #[] ∨ bs = #[]
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_one : Ordinal.lift.{u_2, u_1} 1 = 1
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow_val_succ_eq_mk_add_choose : ∀ (S : Type u_1) [inst : CommRing S] (d : ℕ),
  ↑(PowerSeries.invOneSubPow S (d + 1)) = PowerSeries.mk fun n => ↑((d + n).choose d)
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instInhabitedContext.default : Lean.Meta.Grind.EMatch.Context
-- Mathlib.Algebra.GroupWithZero.Divisibility
isRelPrime_zero_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {x : α}, IsRelPrime 0 x ↔ IsUnit x
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The `S`-torsion submodule is an `S`-torsion module.  -/
Submodule.torsion'_isTorsion' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
  Module.IsTorsion' (↥(Submodule.torsion' R M S)) S
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.equivMvPolynomialQuotient_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R),
  P.equivMvPolynomialQuotient.symm
      ((Ideal.Quotient.mk
          (Ideal.span
            {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f),
              (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)}))
        (MvPolynomial.X 0)) =
    P.X
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_add_left : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α}, IsAddUnit b → b - (a + b) = 0 - a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (i : J.L) (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (match CategoryTheory.Limits.WalkingMulticospan.left i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right i => h_2 i) =
    h_1 i
-- Mathlib.Data.Erased
Erased.join_eq_out : ∀ {α : Sort u_1} (a : Erased (Erased α)), a.join = a.out
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.orbit_inj : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x y : AddAction.orbitRel.Quotient G α},
  x.orbit = y.orbit ↔ x = y
-- Mathlib.Analysis.Normed.Module.DoubleDual
NormedSpace.inclusionInDoubleDualWeak_apply_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (X : Type u_2) [inst_1 : SeminormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (x : WeakSpace 𝕜 X) (x_1 : X →L[𝕜] 𝕜),
  ((NormedSpace.inclusionInDoubleDualWeak 𝕜 X) x) x_1 = x_1 ((toWeakSpace 𝕜 X).symm x)
-- Mathlib.RingTheory.HahnSeries.Summable
/-- The summable family given by multiplying every series in a summable family by a scalar.  -/
HahnSeries.SummableFamily.smulFamily : {Γ : Type u_1} →
  {R : Type u_3} →
    {V : Type u_4} →
      {α : Type u_5} →
        [inst : PartialOrder Γ] →
          [inst_1 : AddCommMonoid R] →
            [inst_2 : AddCommMonoid V] →
              [SMulWithZero R V] → (α → R) → HahnSeries.SummableFamily Γ V α → HahnSeries.SummableFamily Γ V α
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_rel_left : ∀ (a b : ℕ+), ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcd b)
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Prints all characters in a string in hexadecimal with prefix 'U+'.
E.g., "ab" is "U+0061;U+0062".  -/
Mathlib.Linter.TextBased.UnicodeLinter.String.printCodepointHex : String → String
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_map : ∀ {E : Type v} [inst : Field E] (K : Type w) [inst_1 : Field K] (f : Polynomial E) (i : E →+* K),
  (Polynomial.map i f).natSepDegree = f.natSepDegree
-- Mathlib.Combinatorics.Optimization.ValuedCSP
ValuedCSP.Term.mk.injEq : ∀ {D : Type u_1} {C : Type u_2} [inst : AddCommMonoid C] [inst_1 : PartialOrder C] [inst_2 : IsOrderedAddMonoid C]
  {Γ : ValuedCSP D C} {ι : Type u_3} (n : ℕ) (f : (Fin n → D) → C) (inΓ : ⟨n, f⟩ ∈ Γ) (app : Fin n → ι) (n_1 : ℕ)
  (f_1 : (Fin n_1 → D) → C) (inΓ_1 : ⟨n_1, f_1⟩ ∈ Γ) (app_1 : Fin n_1 → ι),
  ({ n := n, f := f, inΓ := inΓ, app := app } = { n := n_1, f := f_1, inΓ := inΓ_1, app := app_1 }) =
    (n = n_1 ∧ f ≍ f_1 ∧ app ≍ app_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g) (e : Y ⟶ Z) (he : CategoryTheory.CategoryStruct.comp f e = 0) {Z_1 : C} (h_1 : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelIsoOfEq h).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f e he) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc g e ⋯) h_1
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_mul : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q ≠ 0 →
        p ≠ 0 →
          q ≠ 0 → AddMonoidAlgebra.supDegree D (p * q) = AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
-- Mathlib.Analysis.Normed.Group.Basic
norm_mul_sub_norm_div_le_two_mul : ∀ {E : Type u_8} [inst : SeminormedGroup E] (u v : E), ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖v‖
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology functor `ShortComplex C ⥤ C` for a category `C` with homology.  -/
CategoryTheory.ShortComplex.homologyFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.CategoryWithHomology C] → CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
-- Mathlib.Algebra.Quandle
/-- The conjugation quandle of a group.  Each element of the group acts by
the corresponding inner automorphism.  -/
Quandle.Conj : Type u_2 → Type u_2
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.CoeAdjoinAux.mem : ∀ {α : Type u_1} {x : α} {s : Set α} [self : Algebra.CoeAdjoinAux x s], x ∈ s
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.reduce : Lean.Meta.ACLt.ReduceMode → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.evalAlgHom_apply : ∀ {X : Type u_1} (S : Type u_2) (R : Type u_3) [inst : TopologicalSpace X] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring R] [inst_3 : Algebra S R] [inst_4 : TopologicalSpace R] [inst_5 : IsTopologicalSemiring R]
  (x : X) (f : C(X, R)), (ContinuousMap.evalAlgHom S R x) f = f x
-- Init.Data.SInt.Bitwise
ISize.or_eq_zero_iff : ∀ {a b : ISize}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Init.Data.Nat.Lemmas
Nat.div_pos_iff : ∀ {a b : ℕ}, 0 < a / b ↔ 0 < b ∧ b ≤ a
-- Batteries.Data.DList.Basic
/-- `O(1)` (`apply` is `O(|l|)`). Convert a `List α` into a `DList α`.  -/
Batteries.DList.ofList : {α : Type u} → List α → Batteries.DList α
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_fun_neg_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.Integrable (fun x => -f x) μ ↔ MeasureTheory.Integrable f μ
-- Lean.Data.Lsp.CodeActions
/-- If the code action is disabled, this type gives the reason why.  -/
Lean.Lsp.CodeActionDisabled : Type
-- Std.Async.UDP
/-- Membership type for multicast operations.
 -/
Std.Async.UDP.Membership : Type
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integral_continuousLinearMap_prod : ∀ {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {mE : MeasurableSpace E} [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.Measure E}
  [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure F} [MeasureTheory.IsProbabilityMeasure ν]
  {L : E × F →L[ℝ] G} [CompleteSpace G],
  MeasureTheory.Integrable id μ →
    MeasureTheory.Integrable id ν →
      ∫ (p : E × F), L p ∂μ.prod ν =
        ∫ (x : E), (L ∘SL ContinuousLinearMap.inl ℝ E F) x ∂μ + ∫ (y : F), (L ∘SL ContinuousLinearMap.inr ℝ E F) y ∂ν
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.erase_add_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : AddMonoidAlgebra R M),
  AddMonoidAlgebra.erase m x + AddMonoidAlgebra.single m (x.coeff m) = x
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- Lebesgue integral of a bounded function over a set of finite measure is finite.
Note that this lemma assumes no regularity of either `f` or `s`.  -/
MeasureTheory.setLIntegral_lt_top_of_le_nnreal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  μ s ≠ ⊤ → ∀ {f : α → ENNReal}, (∃ y, ∀ x ∈ s, f x ≤ ↑y) → ∫⁻ (x : α) in s, f x ∂μ < ⊤
-- Init.Data.BitVec.Lemmas
BitVec.zero_sdiv : ∀ {w : ℕ} {x : BitVec w}, (0#w).sdiv x = 0#w
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.parentDeclCtx.inj : ∀ {parentDecl parentDecl_1 : Lean.Name},
  Lean.Elab.PartialContextInfo.parentDeclCtx parentDecl = Lean.Elab.PartialContextInfo.parentDeclCtx parentDecl_1 →
    parentDecl = parentDecl_1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.instMonoι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f], CategoryTheory.Mono (CategoryTheory.Limits.image.ι f)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.TreeSet.ofList l cmp).get! k = default
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M' → M} {g : M → 𝕜} {y : M}
  {u : Set M} {s : Set M'} (x : M'),
  MDiffAt[u] g y →
    MDiffAt[s] f x →
      f ⁻¹' u ∈ nhdsWithin x s → UniqueMDiffAt[s] x → f x = y → d[s] (g ∘ f) x = d[u] g y ∘SL mfderiv[s] f x
-- Mathlib.Data.List.Cycle
List.prev_getLast_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ x :: l), (x :: l).prev x h = (x :: l).getLast ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.differentiable_arctan : Differentiable ℝ Real.arctan
-- Mathlib.CategoryTheory.Products.Basic
/-- `sectR Z D` is the functor `D ⥤ C × D` given by `Y ↦ (Z, Y)` .  -/
CategoryTheory.Prod.sectR : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    C → (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D (C × D)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β) (f' : α → β)
  (h : f' = ⇑f), f.copy f' h = ↑f
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_fun_neg_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg E],
  (fun x => -f x) =O[𝕜; l] g ↔ f =O[𝕜; l] g
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_eq_top : ∀ {r : ENNReal}, ⌈r⌉ₑ = ⊤ ↔ r = ⊤
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.listSum_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (l : List ι) (f : ι → R),
  (∀ x ∈ l, f x ∈ I) → (List.map f l).sum ∈ I
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
CategoryTheory.FunctorToTypes.monoFactorisation_m : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.Functor C (Type u)} (f : F ⟶ G),
  (CategoryTheory.FunctorToTypes.monoFactorisation f).m = (CategoryTheory.Subfunctor.range f).ι
-- Mathlib.Data.Set.Image
/-- The range of `Option.elim b f` is `{b} ∪ range f`.  -/
Option.range_elim : ∀ {α : Type u_1} {β : Type u_2} (b : β) (f : α → β), (Set.range fun o => o.elim b f) = insert b (Set.range f)
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.aleph0_add_continuum : Cardinal.aleph0 + Cardinal.continuum = Cardinal.continuum
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
/-- A typeclass carrying a choice of bicategorical structural isomorphism between two objects.
Used by the `⊗≫` bicategorical composition operator, and the `coherence` tactic.
 -/
CategoryTheory.BicategoricalCoherence : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : B} → (a ⟶ b) → (a ⟶ b) → Type w
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Left.inv_le_self : ∀ {α : Type u} [inst : Group α] [inst_1 : Preorder α] [MulLeftMono α] {a : α}, 1 ≤ a → a⁻¹ ≤ a
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.isSetAlgebra_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)},
  MeasureTheory.IsSetAlgebra (MeasureTheory.measurableCylinders α)