mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.memLp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : NormedAddCommGroup γ] [BorelSpace γ] {p : ENNReal},
  ProbabilityTheory.IdentDistrib f g μ ν → (MeasureTheory.MemLp f p μ ↔ MeasureTheory.MemLp g p ν)
-- Mathlib.Algebra.Ring.Equiv
/-- Notation for `RingEquiv`.  -/
«term_≃+*_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.yonedaCollectionPresheafToA_val_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  (s : CategoryTheory.yoneda.obj X ⟶ A)
  (p : CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s),
  CategoryTheory.OverPresheafAux.YonedaCollection.fst p.val = s
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesMap_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i],
  HomologicalComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (HomologicalComplex.cyclesMap ψ i)
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.noConfusionType : Sort v✝ → Lean.Json.CompressWorkItemKind✝ → Lean.Json.CompressWorkItemKind✝ → Sort v✝
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- `limsup` over `ℕ` is measurable. See `Measurable.limsup'` for a version with a general filter.
 -/
Measurable.limsup : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {f : ℕ → δ → α}, (∀ (i : ℕ), Measurable (f i)) → Measurable fun x => Filter.limsup (fun i => f i x) Filter.atTop
-- Mathlib.Order.Comparable
incompRel_swap_apply : ∀ {α : Type u_1} {a b : α} (r : α → α → Prop), IncompRel (Function.swap r) a b ↔ IncompRel r a b
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.objects : Lean.Server.FileWorker.RpcSession → Lean.Server.RpcObjectStore
-- Lean.Meta.WHNF
Lean.Meta.reduceNatNative : Lean.Name → Lean.MetaM ℕ
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput.mk.inj : ∀ {term : Lean.Term} {options : Aesop.RuleBuilderOptions} {phase : Aesop.PhaseSpec} {term_1 : Lean.Term}
  {options_1 : Aesop.RuleBuilderOptions} {phase_1 : Aesop.PhaseSpec},
  { term := term, options := options, phase := phase } = { term := term_1, options := options_1, phase := phase_1 } →
    term = term_1 ∧ options = options_1 ∧ phase = phase_1
-- Std.Time.Date.Unit.Month
/-- Determine the `Quarter` by the month.
 -/
Std.Time.Month.Quarter.ofMonth : Std.Time.Month.Ordinal → Std.Time.Month.Quarter
-- Mathlib.Tactic.ProxyType
/-- Name to use for the declaration for the equivalence `proxyType ≃ type`.  -/
Mathlib.ProxyType.ProxyEquivConfig.proxyEquivName : Mathlib.ProxyType.ProxyEquivConfig → Lean.Name
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The outer expression in which the rewrite takes place.  -/
Mathlib.Tactic.ClickSuggestions.GrwInfo.rootExpr : Mathlib.Tactic.ClickSuggestions.GrwInfo → Lean.Expr
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_const_mul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal),
  r ≠ ⊤ → ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentationCore.mk : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            {solution : relations.Solution M} →
              (desc :
                  {N : Type w'} →
                    [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N) →
                (∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N),
                    solution.postcomp (desc s) = s) →
                  (∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
                      solution.postcomp f = solution.postcomp f' → f = f') →
                    solution.IsPresentationCore
-- Mathlib.GroupTheory.Coset.Defs
/-- If two subgroups `M` and `N` of `G` are equal, their quotients are in bijection.  -/
Subgroup.quotientEquivOfEq : {α : Type u_1} → [inst : Group α] → {s t : Subgroup α} → s = t → α ⧸ s ≃ α ⧸ t
-- Lean.Elab.Command
Lean.Elab.Command.State.usedQuotCtxts : Lean.Elab.Command.State → Lean.NameSet
-- Mathlib.Data.Set.Basic
Set.ssubset_iff_subset_ne : ∀ {α : Type u} {s t : Set α}, s ⊂ t ↔ s ⊆ t ∧ s ≠ t
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.not_exists : ∀ {α : Sort u_1} (s : α → Prop), ¬Exists s ↔ ∀ (x : α), binderNameHint x s ¬s x
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- Given a linearly ordered family `v` of vectors of `M` and a natural number `n`, produce the
family of `n`fold exterior products of elements of `v`, seen as members of the exterior algebra.  -/
ExteriorAlgebra.ιMulti_family : (R : Type u1) →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (n : ℕ) → {I : Type u_1} → [LinearOrder I] → (I → M) → ↑(Set.powersetCard I n) → ExteriorAlgebra R M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.RingTheory.Localization.Module
LinearEquiv.extendScalarsOfIsLocalization.congr_simp : ∀ {R : Type u_3} [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (f f_1 : M ≃ₗ[R] N),
  f = f_1 → LinearEquiv.extendScalarsOfIsLocalization S A f = LinearEquiv.extendScalarsOfIsLocalization S_1 A f_1
-- Mathlib.Data.ZMod.Defs
/-- Note this is more general than `Fin.instCommRing` as it applies (vacuously) to `Fin 0` too.  -/
Fin.instHasDistribNeg : (n : ℕ) → HasDistribNeg (Fin n)
-- Lean.Meta.GeneralizeVars
_private.Lean.Meta.GeneralizeVars.0.Lean.Meta.mkGeneralizationForbiddenSet.visit : Lean.FVarId → List Lean.FVarId → Lean.FVarIdSet → Lean.MetaM (List Lean.FVarId × Lean.FVarIdSet)
-- Mathlib.Order.SuccPred.Basic
Order.succ_pred_of_not_isMin : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : PredOrder α] {a : α},
  ¬IsMin a → Order.succ (Order.pred a) = a
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the largest element of the tree set, returning `fallback` if the tree set is empty.
 -/
Std.TreeSet.Raw.maxD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → α
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optTypeForStructInst.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.FieldTheory.PurelyInseparable.Basic
isPurelyInseparable_self : ∀ (F : Type u_1) [inst : CommRing F], IsPurelyInseparable F F
-- Mathlib.Data.EReal.Inv
EReal.abs_top : ⊤.abs = ⊤
-- Mathlib.Data.FunLike.Group
FunLike.coeMonoidHom_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : MulOne F] [inst_2 : MulOneClass β]
  [inst_3 : IsOneApply F α β] [inst_4 : IsMulApply F α β], Function.Injective ⇑(FunLike.coeMonoidHom F α β)
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- If a function is `C^2` at a point, then its second derivative there is symmetric. Over a field
different from `ℝ` or `ℂ`, we should require that the function is analytic.  -/
ContDiffAt.isSymmSndFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → minSmoothness 𝕜 2 ≤ n → IsSymmSndFDerivAt 𝕜 f x
-- Init.Data.UInt.Bitwise
UInt64.or_assoc : ∀ (a b c : UInt64), a ||| b ||| c = a ||| (b ||| c)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.isIso_prod_iff : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P Q : C} {S T : D} {f : (P, S) ⟶ (Q, T)},
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.1 ∧ CategoryTheory.IsIso f.2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeKind.comment : Lean.Lsp.FoldingRangeKind
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.of_equiv : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (e : SymmetricAlgebra R M ≃ₐ[R] A),
  ↑↑e ∘ₗ SymmetricAlgebra.ι R M = f → IsSymmetricAlgebra f
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.aleph_ord : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Cardinal.aleph c.ord = c
-- Mathlib.SetTheory.ZFC.Ordinal
_private.Mathlib.SetTheory.ZFC.Ordinal.0.Ordinal.toZFSet_mem_toZFSet_of_lt : ∀ {a b : Ordinal.{u_1}}, a < b → a.toZFSet ∈ b.toZFSet
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.noConfusionType : Sort v✝ → Lean.Lsp.CompletionItemKind → Lean.Lsp.CompletionItemKind → Sort v✝
-- Mathlib.Computability.TuringMachine.Computable
/-- a main function: the initial function that is executed, given by its label  -/
Turing.FinTM2.main : (self : Turing.FinTM2) → self.Λ
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- An equivalence of group extensions from a homomorphism making a commuting diagram. Such a
homomorphism is necessarily an isomorphism.  -/
GroupExtension.Equiv.ofMonoidHom : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] →
        {E : Type u_3} →
          [inst_2 : Group E] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} →
                [inst_3 : Group E'] →
                  {S' : GroupExtension N E' G} →
                    (f : E →* E') → f.comp S.inl = S'.inl → S'.rightHom.comp f = S.rightHom → S.Equiv S'
-- Mathlib.Topology.MetricSpace.Cauchy
/-- In a pseudometric space, uniform Cauchy sequences are characterized by the fact that,
eventually, the distance between all its elements is uniformly, arbitrarily small.  -/
Metric.uniformCauchySeqOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {γ : Type u_3}
  {F : β → γ → α} {s : Set γ},
  UniformCauchySeqOn F Filter.atTop s ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_7 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (k : ℕ) (cf cg : Nat.Partrec.Code)
  (h_1 : (x : Nat.Partrec.Code) → motive 0 x) (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero)
  (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ) (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left)
  (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match k.succ, cf.comp cg with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_7 k cf cg
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.anyLTTR.loop.eq_def : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (i : ℕ) (a : i ≤ n),
  Nat.anyLTTR.loop✝ n f i a =
    match i, a with
    | 0, x => false
    | i.succ, h => f (n - (i + 1)) ⋯ || Nat.anyLTTR.loop✝ n f i ⋯
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleCore_coordChange_model_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} (x x' z : H),
  (tangentBundleCore I H).coordChange (achart H x) (achart H x') z = ContinuousLinearMap.id 𝕜 E
-- Mathlib.LinearAlgebra.Lagrange
/-- This is the characteristic property of the interpolation: the interpolation is the
unique polynomial of `degree < Fintype.card ι` which takes the value of the `r i` on the `v i`.
 -/
Lagrange.eq_interpolate_iff : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F)
  {f : Polynomial F},
  Set.InjOn v ↑s → ((f.degree < ↑s.card ∧ ∀ i ∈ s, Polynomial.eval (v i) f = r i) ↔ f = (Lagrange.interpolate s v) r)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- Help the typechecker by converting a point in a groupoid back to a point in
the underlying topological space.  -/
FundamentalGroupoid.toTop : {X : TopCat} → ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj X) → ↑X
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.directSum_iff : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)], Module.Flat R (DirectSum ι fun i => M i) ↔ ∀ (i : ι), Module.Flat R (M i)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- Construct a `Subring R` from a set `s`, a submonoid `sm`, and an additive
subgroup `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`.  -/
Subring.mk' : {R : Type u} →
  [inst : NonAssocRing R] → (s : Set R) → (sm : Submonoid R) → (sa : AddSubgroup R) → ↑sm = s → ↑sa = s → Subring R
-- Mathlib.ModelTheory.Satisfiability
/-- A version of The Downward Löwenheim–Skolem theorem where the structure `N` elementarily embeds
into `M`, but is not by type a substructure of `M`, and thus can be chosen to belong to the universe
of the cardinal `κ`.
 -/
FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] (κ : Cardinal.{w}),
  Cardinal.aleph0 ≤ κ →
    Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
      Cardinal.lift.{w', w} κ ≤ Cardinal.lift.{w, w'} (Cardinal.mk M) →
        ∃ N, Nonempty (L.ElementaryEmbedding (↑N) M) ∧ Cardinal.mk ↑N = κ
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Multiset.esymm_pair_one : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R), (x ::ₘ {y}).esymm 1 = x + y
-- Mathlib.Condensed.Light.Sequence
LightCondensed.internallyProjective_free_natUnionInfty : ∀ (R : Type) [inst : CommRing R],
  CategoryTheory.InternallyProjective ((LightCondensed.free R).obj LightProfinite.NatUnionInfty.toCondensed)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapM_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.filterMapM f it)).toArray =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => some <$> g fb)
        it).toArray
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsCircuit.contract_dep : ∀ {α : Type u_1} {M : Matroid α} {K C : Set α}, M.IsCircuit K → Disjoint C K → (M.contract C).Dep K
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValRat_def : ∀ (p : ℕ) (q : ℚ), padicValRat p q = ↑(padicValInt p q.num) - ↑(padicValNat p q.den)
-- Init.Data.Float.Model.Unpacked.Sign
/-- Positive (`+`) sign.  -/
Float.Model.UnpackedFloat.Sign.positive : Float.Model.UnpackedFloat.Sign
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- A `Valued` version of `Valuation.integer`, enabling the notation `𝒪[K]` for the
valuation integers of a valued field `K`.  -/
Valued.integer : (K : Type u_1) →
  [inst : Field K] →
    {Γ₀ : outParam (Type u_2)} → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → [vK : Valued K Γ₀] → Subring K
-- Mathlib.Logic.Equiv.Bool
Bool.not_surjective : Function.Surjective not
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Methods.mk : (Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)) →
  (Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr)) →
    (Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) →
      (Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) →
        (Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) →
          (Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) →
            (Lean.Expr → Lean.MetaM (ℤ × Lean.Expr × Lean.Expr)) →
              (ℤ → Lean.MetaM Lean.Expr) → Mathlib.Tactic.IntervalCases.Methods
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanHom_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {B : Set β} {f : α → β} {n : ℕ},
  IsMulFreimanHom n ∅ B f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_union!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  (contains_right : Std.DTreeMap.Internal.Impl.contains k m₂ = true), (m₁.union! m₂).get k ⋯ = m₂.get k contains_right
-- Lean.Meta.HaveTelescope
/-- A cached version of the telescope body's type, instantiated with fvars from each `HaveInfo.decl`.  -/
Lean.Meta.HaveTelescopeInfo.bodyType : Lean.Meta.HaveTelescopeInfo → Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The functor which sends a simplicial set to the type of its connected components.  -/
SSet.π₀Functor : CategoryTheory.Functor SSet (Type u)
-- Mathlib.Condensed.Functors
/-- The yoneda presheaf as a condensed set, restricted to profinite spaces.  -/
profiniteToCondensed : CategoryTheory.Functor Profinite CondensedSet
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.natAbs_abs : ∀ (a : ℤ), |a|.natAbs = a.natAbs
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- The last case which has type `(cooper_*_split ... 0)`  -/
Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.last : Array (Lean.FVarId × Lean.Meta.Grind.Arith.Cutsat.UnsatProof) →
  Array Lean.FVarId → Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.condition : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) [inst_2 : CategoryTheory.Limits.HasEnd F] {i j : J}
  (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F i) ((F.obj (Opposite.op i)).map f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F j) ((F.map f.op).app j)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instIsProbabilityMeasure : ∀ {α : Type u_4} {β : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν],
  MeasureTheory.IsProbabilityMeasure (μ.prod ν)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.min? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ y⁻¹ * x` is quasi-measure-preserving.  -/
MeasureTheory.quasiMeasurePreserving_inv_mul_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.2⁻¹ * p.1) (μ.prod ν) μ
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.minpoly_powerBasis_gen : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} (hf : f ≠ 0),
  minpoly K (AdjoinRoot.powerBasis hf).gen = f * Polynomial.C f.leadingCoeff⁻¹
-- Mathlib.Data.ENNReal.Real
ENNReal.lt_ofReal_iff_toReal_lt : ∀ {a : ENNReal} {b : ℝ}, a ≠ ⊤ → (a < ENNReal.ofReal b ↔ a.toReal < b)
-- Init.Data.Vector.Lemmas
Vector.getElem?_swap : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (hi : i < n) (hj : j < n) {k : ℕ},
  (xs.swap i j hi hj)[k]? = if j = k then some xs[i] else if i = k then some xs[j] else xs[k]?
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherianRing_of_surjective : ∀ (R : Type u_1) [inst : Semiring R] (S : Type u_2) [inst_1 : Semiring S] (f : R →+* S),
  Function.Surjective ⇑f → ∀ [H : IsNoetherianRing R], IsNoetherianRing S
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually
commute then `NormedSpace.exp (∑ i, f i) = ∏ i, NormedSpace.exp (f i)`.  -/
NormedSpace.exp_sum_of_commute : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {ι : Type u_3} (s : Finset ι) (f : ι → 𝔸)
  (h : (↑s).Pairwise (Function.onFun Commute f)),
  NormedSpace.exp (∑ i ∈ s, f i) = s.noncommProd (fun i => NormedSpace.exp (f i)) ⋯
-- Batteries.Data.List.Basic
List.forDiagM.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → α → m PUnit.{u_1 + 1}) (a : α) (l : List α),
  List.forDiagM f (a :: l) = do
    f a a
    l.forM (f a)
    List.forDiagM f l
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.EqId.eq_1 : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  A.EqId = (A = CategoryTheory.SimplicialObject.Splitting.IndexSet.id Δ)
-- Init.Data.Fin.Lemmas
Fin.mk_lt_of_lt_val : ∀ {n : ℕ} {b : Fin n} {a : ℕ} (h : a < ↑b), ⟨a, ⋯⟩ < b
-- Mathlib.Data.Finset.Range
Finset.mem_range_sub_ne_zero : ∀ {n x : ℕ}, x ∈ Finset.range n → n - x ≠ 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.unitOfList_eq_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α},
  Std.ExtTreeMap.unitOfList l cmp = List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l
-- Lean.Compiler.InitAttr
/-- Run the initializer of the given module (without `builtin_initialize` commands).
Return `false` if the initializer is not available as native code.
Initializers do not have corresponding Lean definitions, so they cannot be interpreted in this case.
 -/
_private.Lean.Compiler.InitAttr.0.Lean.runModInit : Lean.Name → Option String → Lean.IRPhases → IO Bool
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsPlot.dSmooth_comp' : ∀ {X : Type u_1} {Y : Type u_2} [inst : DiffeologicalSpace X] [inst_1 : DiffeologicalSpace Y] {n : ℕ}
  {p : EuclideanSpace ℝ (Fin n) → X} {f : X → Y},
  Diffeology.IsPlot p → Diffeology.DSmooth f → Diffeology.IsPlot fun x => f (p x)