mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.sset.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {i offset : ℕ} {y : Lean.FVarId} {ty : Lean.Expr}
  {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_11} {fvarId_1 : Lean.FVarId}
  {i_1 offset_1 : ℕ} {y_1 : Lean.FVarId} {ty_1 : Lean.Expr} {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_11},
  Lean.Compiler.LCNF.Code.sset fvarId i offset y ty k h =
      Lean.Compiler.LCNF.Code.sset fvarId_1 i_1 offset_1 y_1 ty_1 k_1 h_1 →
    fvarId = fvarId_1 ∧ i = i_1 ∧ offset = offset_1 ∧ y = y_1 ∧ ty = ty_1 ∧ k = k_1
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
hasFDerivWithinAt_comp_smul_iff_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {f' : E →L[𝕜] F} {x : E} {c : 𝕜},
  c ≠ 0 → (HasFDerivWithinAt (fun x => f (c • x)) f' s x ↔ HasFDerivWithinAt (c • f) f' (c • s) (c • x))
-- Mathlib.Algebra.BigOperators.WithTop
/-- A product of finite terms is finite.  -/
WithTop.prod_ne_top : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
  [inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀}, (∀ i ∈ s, f i ≠ ⊤) → ∏ i ∈ s, f i ≠ ⊤
-- Mathlib.RingTheory.TensorProduct.Basic
LinearMap.liftBaseChangeEquiv_symm_apply : ∀ {R : Type u_4} {M : Type u_2} {N : Type u_3} (A : Type u_1) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module A N] [inst_8 : IsScalarTower R A N] (l : TensorProduct R A M →ₗ[A] N) (x : M),
  ((LinearMap.liftBaseChangeEquiv A).symm l) x = l (1 ⊗ₜ[R] x)
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.of_image : ∀ {α : Type u} {β : Type v} (f : α → β) {s : Set α}, (f '' s).Infinite → s.Infinite
-- Mathlib.Analysis.Complex.Basic
Complex.hasSum_conj' : ∀ {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ},
  HasSum (fun x => (starRingEnd ℂ) (f x)) ((starRingEnd ℂ) x) L ↔ HasSum f x L
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_some_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {k : α},
  m.contains k = true → m.get? k = some k
-- Aesop.Search.Expansion.Norm
Aesop.NormM.State.mk : Aesop.ForwardState → Aesop.ForwardRuleMatches → Aesop.NormM.State
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.comp_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y : C}
  (f : W ⟶ X) (g : X ⟶ Y) (Z : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Z =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z)
-- Batteries.Lean.Expr
/-- Like `getAppRevArgs` but ignores metadata.  -/
Lean.Expr.getAppRevArgs' : Lean.Expr → Array Lean.Expr
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.toEmbedding.eq_1 : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.PartialEquiv M N), f.toEmbedding = f.cod.subtype.comp f.toEquiv.toEmbedding
-- Mathlib.MeasureTheory.Measure.Regular
Set.exists_isOpen_le_add : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] (A : Set α) (μ : MeasureTheory.Measure α)
  [μ.OuterRegular] {ε : ENNReal}, ε ≠ 0 → ∃ U ⊇ A, IsOpen U ∧ μ U ≤ μ A + ε
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.domRestrict_apply : ∀ {M : Type u_1} {σ : Type u_4} [inst : Add M] {N : Type u_5} [inst_1 : Add N] [inst_2 : SetLike σ M]
  [inst_3 : AddMemClass σ M] (f : M →ₙ+ N) {S : σ} (x : ↥S), (f.domRestrict S) x = f ↑x
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Computation.Corec.f.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (val : β) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (val : β) → motive (Sum.inr val)),
  (match Sum.inr val with
    | Sum.inl a => h_1 a
    | Sum.inr val => h_2 val) =
    h_2 val
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.foldBranchesM : {σ : Type u_1} →
  {m : Type u_1 → Type u_2} → [Monad m] → (σ → Aesop.Frontend.Feature → m σ) → σ → Aesop.Frontend.RuleExpr → m (Array σ)
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.of_diffs_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α},
  (s.diffs t).Nonempty → t.Nonempty
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- Given `R : C`, this is the functor `SSet.{w} ⥤ ChainComplex C ℕ` which sends
a simplicial set `X` to `X.normalizedChainComplex R`.  -/
SSet.normalizedChainComplexFunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] → C → CategoryTheory.Functor SSet (ChainComplex C ℕ)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set `D f K` is a complicated set constructed using countable intersections and unions. Its
main use is that, when `K` is complete, it is exactly the set of points where `f` is differentiable,
with a derivative in `K`.  -/
RightDerivMeasurableAux.D : {F : Type u_1} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (ℝ → F) → Set F → Set ℝ
-- Mathlib.Order.Heyting.Hom
CoheytingHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] {f g : CoheytingHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult : Inhabited Mathlib.Tactic.BicategoryLike.Eval.Result
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.instIsCofilteredOrEmptyProd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofilteredOrEmpty C] [CategoryTheory.IsCofilteredOrEmpty D],
  CategoryTheory.IsCofilteredOrEmpty (C × D)
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons of different weights, strict inequality
version: there is a pigeonhole with the total weight of pigeons in it less than `b` provided that
the total number of pigeonholes times `b` is greater than the total weight of all pigeons.  -/
Fintype.exists_sum_fiber_lt_of_sum_lt_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {w : α → M} {b : M} [inst_3 : AddCommMonoid M] [inst_4 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  ∑ x, w x < Fintype.card β • b → ∃ y, ∑ x with f x = y, w x < b
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Warning: Creates a typeclass loop with `MeasurableSingletonClass.toDiscreteMeasurableSpace`.
To be monitored.  -/
DiscreteMeasurableSpace.toMeasurableSingletonClass : ∀ {α : Type u_1} [inst : MeasurableSpace α] [DiscreteMeasurableSpace α], MeasurableSingletonClass α
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelUnitReal.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel Unit (α × ℝ))
  [inst : ProbabilityTheory.IsFiniteKernel κ],
  κ.condKernelUnitReal = ProbabilityTheory.IsCondKernelCDF.toKernel (fun p => ProbabilityTheory.condCDF (κ ()) p.2) ⋯
-- Mathlib.Order.GaloisConnection.Defs
/-- If there exists a `b` such that `a = u a`, then `b = l a` is one such element.  -/
GaloisConnection.exists_eq_u : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ (a : α), (∃ b, a = u b) ↔ a = u (l a)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M},
  CliffordAlgebra.reverse = ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ CliffordAlgebra.reverseOp.toLinearMap
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₁'_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₁'.g = S.δ
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Iic b` and monotone on `Ico b a`, then the minimum of `f` on `Iio a`
is attained at `b`.  -/
isMinOn_Iio_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  AntitoneOn f (Set.Iic b) → MonotoneOn f (Set.Ico b a) → IsMinOn f (Set.Iio a) b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
cfcL.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {p p_1 : A → Prop} (e_p : p = p_1) [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A]
  [inst_6 : Ring A] [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A}
  (ha : p a), cfcL ha = cfcL ⋯
-- Mathlib.Analysis.ConstantSpeed
HasConstantSpeedOnWith.union : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} {t : Set ℝ},
  HasConstantSpeedOnWith f s l →
    HasConstantSpeedOnWith f t l → ∀ {x : ℝ}, IsGreatest s x → IsLeast t x → HasConstantSpeedOnWith f (s ∪ t) l
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_setWidth_of_le : ∀ {w : ℕ} {b : BitVec w} {start len w' : ℕ},
  start + len ≤ w' → BitVec.extractLsb' start len (BitVec.setWidth w' b) = BitVec.extractLsb' start len b
-- Init.Data.Vector.Lemmas
Vector.set_getElem_self : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} (hi : i < n), xs.set i xs[i] hi = xs
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_of_isUnit : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {x : α},
  IsUnit x → UniqueFactorizationMonoid.factors x = 0
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The right whiskering of an isomorphism is an isomorphism.  -/
CategoryTheory.MonoidalCategory.whiskerRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        (X ≅ Y) →
          (Z : C) →
            CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv =
    (CategoryTheory.Functor.LaxMonoidal.ε F).unmop.app d
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_map_sectR : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (c : α) (a b : β),
  Finset.map (Function.Embedding.sectR c β) (Finset.Ioc a b) = Finset.Ioc (c, a) (c, b)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swap.match_1.eq_5 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (a : α) (xs : List α) (i j : ℕ)
  (h_1 : (x x_1 : ℕ) → motive [] x x_1) (h_2 : (a : α) → (xs : List α) → motive (a :: xs) 0 0)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) 0 i.succ)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → motive (a :: xs) i.succ 0)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → motive (a :: xs) i.succ j.succ),
  (match a :: xs, i.succ, j.succ with
    | [], x, x_1 => h_1 x x_1
    | a :: xs, 0, 0 => h_2 a xs
    | a :: xs, 0, i.succ => h_3 a xs i
    | a :: xs, i.succ, 0 => h_4 a xs i
    | a :: xs, i.succ, j.succ => h_5 a xs i j) =
    h_5 a xs i j
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from commutative monoids to types preserves all limits.  -/
CommMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget MonCat)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fundamentalSequenceProp_inr : ∀ (o : ONote) (f : ℕ → ONote),
  o.FundamentalSequenceProp (Sum.inr f) ↔
    Order.IsSuccLimit o.repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < o ∧ (o.NF → (f i).NF)) ∧ ∀ a < o.repr, ∃ i, a < (f i).repr
-- Mathlib.Data.Finsupp.Basic
Finsupp.prod_sumElim : ∀ {ι₁ : Type u_12} {ι₂ : Type u_13} {α : Type u_14} {M : Type u_15} [inst : Zero α] [inst_1 : CommMonoid M]
  (f₁ : ι₁ →₀ α) (f₂ : ι₂ →₀ α) (g : ι₁ ⊕ ι₂ → α → M),
  (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr)
-- Lean.Elab.BuiltinCommand
/-- Helper for `findSuffixWithPrefix`. If `allowOffset` is `false`, then `seg` must be a suffix of
`base`, not just a prefix of a suffix.
 -/
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.findSuffixWithPrefix.findSuffixMatch : Lean.Name → Lean.Name → Bool → Option Lean.Name
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.WeierstrassCurve.Jacobian.toAffine_negAddY_of_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    ∀ {n d : F},
      d ≠ 0 →
        W.toAffine.negAddY (P 0 / P 2 ^ 2) (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) (-n / (P 2 * d)) =
          (-n * (n ^ 2 - W.a₁ * n * P 2 * d - W.a₂ * P 2 ^ 2 * d ^ 2 - 2 * P 0 * d ^ 2 - P 0 * d ^ 2) + P 1 * d ^ 3) /
            (P 2 * d) ^ 3
-- Mathlib.Logic.Equiv.Defs
Equiv.eq_symm_iff_trans_eq_refl : ∀ {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α}, f = g.symm ↔ f.trans g = Equiv.refl α
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_shiftRight : ∀ (a b : ISize) (h : System.Platform.numBits = 64),
  (a >>> b).toBitVec64 h = (a.toBitVec64 h).sshiftRight' ((b.toBitVec64 h).smod 64)
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
/-- For nonzero `a₁` and `a₂`, `frobeniusRotation a₁ a₂` is a Witt vector that satisfies the
equation `frobenius (frobeniusRotation a₁ a₂) * a₁ = (frobeniusRotation a₁ a₂) * a₂`.
 -/
WittVector.frobeniusRotation : (p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst : Field k] →
        [CharP k p] → [IsAlgClosed k] → {a₁ a₂ : WittVector p k} → a₁.coeff 0 ≠ 0 → a₂.coeff 0 ≠ 0 → WittVector p k
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm5b : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_zero_X_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R) (s : σ),
  (MvPowerSeries.coeff 0) (MvPowerSeries.X s * φ) = 0
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.PreservesColimitOfIsReflexivePair.out : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  {G : CategoryTheory.Functor C D} [self : CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G] ⦃A B : C⦄
  (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.Topology.Sets.VietorisTopology
/-- **Alias** of `TopologicalSpace.NonemptyCompacts.isOpen_setOfPred_disjoint_coe`. -/
TopologicalSpace.NonemptyCompacts.isOpen_setOf_disjoint_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], IsOpen {p | Disjoint ↑p.1 ↑p.2}
-- Mathlib.Algebra.Group.Irreducible.Defs
AddIrreducible.mk : ∀ {M : Type u_1} [inst : AddMonoid M] {p : M},
  ¬IsAddUnit p → (∀ ⦃a b : M⦄, p = a + b → IsAddUnit a ∨ IsAddUnit b) → AddIrreducible p
-- Mathlib.Order.OrderDual
OrderDual.instDecidableEq : (α : Type u_2) → [DecidableEq α] → DecidableEq αᵒᵈ
-- Lean.DocString.Markdown
/-- Renders an `Inline i` to its Markdown lines. The `InlineCtx` argument tracks which inline delimiters
are already open so that nested `*` / `**` / `[…](…)` don't emit redundant openers and closers. The
top level is represented by `{}`.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.inlineMarkdown : {i : Type u_1} →
  [Lean.Doc.MarkdownInline i] → Lean.Doc.MarkdownM.InlineCtx → Lean.Doc.Inline i → Lean.Doc.MarkdownM (Array String)
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousWithinAt.zpow₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] [ContinuousMul G₀]
  {X : Type u_4} [inst_4 : TopologicalSpace X] {a : X} {s : Set X} {f : X → G₀},
  ContinuousWithinAt f s a → ∀ (m : ℤ), f a ≠ 0 ∨ 0 ≤ m → ContinuousWithinAt (fun x => f x ^ m) s a
-- Init.Data.List.Lemmas
List.head?_flatten : ∀ {α : Type u_1} {L : List (List α)}, L.flatten.head? = List.findSome? (fun l => l.head?) L
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.StrictPatternModel.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat],
  ¬String.Slice.Pattern.Model.PatternModel.Matches pat "" → String.Slice.Pattern.Model.StrictPatternModel pat
-- Mathlib.Data.Holor
Holor.cprankMax_sum : ∀ {α : Type} {ds : List ℕ} [inst : NonUnitalNonAssocSemiring α] {β : Type u_1} {n : ℕ} (s : Finset β)
  (f : β → Holor α ds), (∀ x ∈ s, Holor.CPRankMax n (f x)) → Holor.CPRankMax (s.card * n) (∑ x ∈ s, f x)
-- Init.Data.String.Lemmas.IsEmpty
String.copy_slice_self : ∀ {s : String} {p : s.Pos}, (s.slice p p ⋯).copy = ""
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
/-- The symmetry isomorphism `K.flip.total c ≅ K.total c` of the total complex of a
bicomplex when we have `[TotalComplexShapeSymmetry c₁ c₂ c]`.  -/
HomologicalComplex₂.totalFlipIso : {C : Type u_1} →
  {I₁ : Type u_2} →
    {I₂ : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Preadditive C] →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  (c : ComplexShape J) →
                    [inst_2 : TotalComplexShape c₁ c₂ c] →
                      [inst_3 : TotalComplexShape c₂ c₁ c] →
                        [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] →
                          [inst_5 : K.HasTotal c] → [inst_6 : DecidableEq J] → K.flip.total c ≅ K.total c
-- Mathlib.Order.Lattice
DistribLattice.toLattice : {α : Type u_1} → [self : DistribLattice α] → Lattice α
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instHasPullbacksAffineEtale : ∀ (S : AlgebraicGeometry.Scheme), CategoryTheory.Limits.HasPullbacks S.AffineEtale
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.sl_moeb : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  g • z = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g) • z
-- Mathlib.Order.Bounds.Basic
/-- If `a` is the greatest lower bound of `s` and `b` is the greatest lower bound of `t`,
then `a ⊓ b` is the greatest lower bound of `s ∪ t`.  -/
IsGLB.union : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] {a b : γ} {s t : Set γ}, IsGLB s a → IsGLB t b → IsGLB (s ∪ t) (a ⊓ b)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (hom hom_1 : X ⟶ Y) (e_hom : hom = hom_1)
  (inv inv_1 : Y ⟶ X) (e_inv : inv = inv_1)
  (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X)
  (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y),
  { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } =
    { hom := hom_1, inv := inv_1, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosedIn.isIntegral_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsIntegrallyClosedIn R A] {x : A}, IsIntegral R x ↔ ∃ y, (algebraMap R A) y = x
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The opposite category of `WithInitial C` is equivalent to `WithTerminal Cᵒᵖ`.  -/
CategoryTheory.WithInitial.opEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → (CategoryTheory.WithInitial C)ᵒᵖ ≌ CategoryTheory.WithTerminal Cᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Removing leaves from a connected graph keeps it connected.  -/
SimpleGraph.Preconnected.induce_of_degree_eq_one : ∀ {V : Type u} {G : SimpleGraph V},
  G.Preconnected → ∀ {s : Set V}, (∀ v ∉ s, (G.neighborSet v).Subsingleton) → (SimpleGraph.induce s G).Preconnected
-- Aesop.Forward.State
/-- Returns the set of matches and hypotheses associated with a slot `slot`
with instantiation `inst`.  -/
Aesop.InstMap.find? : Aesop.InstMap → Aesop.SlotIndex → Lean.Expr → Lean.MetaM (Option (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp))
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleHeaderDecls : Type
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula for derivatives**, assuming `f` is continuous on a closed ball and
differentiable on its interior away from a countable set.  -/
Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ}
  {s : Set ℂ},
  0 < R →
    ∀ (n : ℕ),
      s.Countable →
        ContinuousOn f (Metric.closedBall c R) →
          (∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) →
            ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
              (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c
-- Mathlib.Analysis.Calculus.Deriv.Abs
differentiableAt_abs_neg : ∀ {x : ℝ}, x < 0 → DifferentiableAt ℝ (fun x => |x|) x
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.coe_val_inv_equivUnits_apply : ∀ {G : Type u_1} [inst : Add G] {a : G} (a_1 : AddConstEquiv G G a a) (a_2 : G),
  ↑(AddConstEquiv.equivUnits a_1)⁻¹ a_2 = a_1⁻¹ a_2
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.mk : ∀ {S : Set ℕ} {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  (∀ {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n) →
    (∀ (x : B), x ∈ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) → IsCyclotomicExtension S A B
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_uIcc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.rev (Finset.uIcc i j) = Finset.uIcc i.rev j.rev
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.restrict_isBase : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → (M.restrict X).IsBase I
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- On a local site, every covering sieve contains every morphism from the terminal object.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.from_terminal_mem_of_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.IsLocalSite] {X : C} (f : ⊤_ C ⟶ X) {S : CategoryTheory.Sieve X}, S ∈ J X → S.arrows f
-- Mathlib.AlgebraicGeometry.Stalk
/-- Copy of `isLocalHom_stalkClosedPointTo` which unbundles the comm ring.

Useful for use in combination with `CommRingCat.of K` for a field `K`.
 -/
AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo' : ∀ {X : AlgebraicGeometry.Scheme} {R : Type u} [inst : CommRing R] [inst_1 : IsLocalRing R]
  (f : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ X),
  IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.stalkClosedPointTo f))