mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasRightHomology]
  [inst_6 : S₂.HasRightHomology] [inst_7 : F.PreservesRightHomologyOf S₁] [inst_8 : F.PreservesRightHomologyOf S₂]
  {Z : D} (h : F.obj S₂.rightHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapRightHomologyIso F).hom h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ)) h)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.vaddConst_symm_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (b p' : P₁), (AffineEquiv.vaddConst k b).symm p' = p' -ᵥ b
-- Lean.Linter.Init
/-- Register a builtin linter set entry. Only valid during initialization;
use `register_builtin_linter_set` rather than calling this directly.  -/
Lean.Linter.addBuiltinLinterSet : Lean.Name → Lean.NameSet → IO Unit
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.vadd.eq_1 : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : ContinuousConstVAdd G α] (γ : G),
  Homeomorph.vadd γ = { toEquiv := AddAction.toPerm γ, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.SetTheory.ZFC.PSet
PSet.nonempty_of_mem : ∀ {x u : PSet.{u_1}}, x ∈ u → u.Nonempty
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.zero.eq_1 : Tactic.ComputeAsymptotics.MultiseriesExpansion.zero = Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal 0
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], { coeff := 0 } = 0
-- Mathlib.Algebra.Field.Opposite
AddOpposite.instRatCast : {α : Type u_1} → [RatCast α] → RatCast αᵃᵒᵖ
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the reverse direction of `absorbs_iUnion`. -/
Absorbs.iUnion : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Sort u_3} [Finite ι]
  {t : ι → Set α}, (∀ (i : ι), Absorbs M s (t i)) → Absorbs M s (⋃ i, t i)
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM.State.mk.injEq : ∀ (script : Aesop.Script.UScript) (proofHasMVar : Bool) (script_1 : Aesop.Script.UScript) (proofHasMVar_1 : Bool),
  ({ script := script, proofHasMVar := proofHasMVar } = { script := script_1, proofHasMVar := proofHasMVar_1 }) =
    (script = script_1 ∧ proofHasMVar = proofHasMVar_1)
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearEquiv.integral_comp_comm : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  [inst_1 : RCLike 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace ℝ F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : NormedSpace ℝ E] (L : E ≃L[𝕜] F) (φ : X → E),
  ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_div : ∀ (r s : ℝ), ↑(r / s) = ↑r / ↑s
-- Lean.ErrorExplanation
Lean.ErrorExplanation.Metadata.mk.sizeOf_spec : ∀ (summary sinceVersion : String) (severity : Lean.MessageSeverity) (removedVersion? : Option String),
  sizeOf
      { summary := summary, sinceVersion := sinceVersion, severity := severity, removedVersion? := removedVersion? } =
    1 + sizeOf summary + sizeOf sinceVersion + sizeOf severity + sizeOf removedVersion?
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C]
  (toPresheafedSpace : AlgebraicGeometry.PresheafedSpace C) (IsSheaf : toPresheafedSpace.presheaf.IsSheaf),
  sizeOf { toPresheafedSpace := toPresheafedSpace, IsSheaf := IsSheaf } = 1 + sizeOf toPresheafedSpace
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.self_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  A.LinearDisjoint F
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.trans_abs_le : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [inst : TopologicalSpace β] [inst_1 : CommRing β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Asymptotics.SuperpolynomialDecay l k f → (∀ (x : α), |g x| ≤ |f x|) → Asymptotics.SuperpolynomialDecay l k g
-- Mathlib.Probability.Distributions.SetBernoulli
/-- The product of bernoulli distributions with parameter `p` on the set `u : Set V` is the measure
on `Set V` such that each element of `u` is taken with probability `p`, and the elements outside of
`u` are never taken.  -/
ProbabilityTheory.setBernoulli : {ι : Type u_1} → Set ι → ↑unitInterval → MeasureTheory.Measure (Set ι)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_ground : ∀ {α : Type u_1} {X : Set α} {M : Matroid α}, (M.restrictSubtype X).E = Set.univ
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.pi.eq_1 : ∀ {𝕜 : Type u} {E : Type v} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] {ι : Type u_1}
  {F : ι → Type u_2} [inst_6 : (i : ι) → AddCommGroup (F i)] [inst_7 : (i : ι) → Module 𝕜 (F i)]
  [inst_8 : (i : ι) → TopologicalSpace (F i)] [inst_9 : ∀ (i : ι), IsTopologicalAddGroup (F i)]
  [inst_10 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] (p : (i : ι) → FormalMultilinearSeries 𝕜 E (F i)) (x : ℕ),
  FormalMultilinearSeries.pi p x = ContinuousMultilinearMap.pi fun i => p i x
-- Lean.Data.JsonRpc
/-- A primitive or structured value that contains additional
information about the error. Can be omitted.  -/
Lean.JsonRpc.ResponseError.data? : {α : Type u} → Lean.JsonRpc.ResponseError α → Option α
-- Mathlib.Order.Heyting.Basic
sdiff_le_comm : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, c \ b ≤ a ↔ c \ a ≤ b
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_mul_distrib_aux : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A B : Matrix n n α),
  IsLeftRegular A.det → IsLeftRegular B.det → (A * B).adjugate = B.adjugate * A.adjugate
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_of_notMem_incidenceSet : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : MulZeroOneClass R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {a : α} {e : Sym2 α}, e ∉ G.incidenceSet a → SimpleGraph.incMatrix R G a e = 0
-- Mathlib.RingTheory.HahnSeries.Lex
/-- For `Archimedean` coefficients, there is a correspondence between finite
archimedean classes and `HahnSeries.orderTop` without the top element.  -/
HahnSeries.finiteArchimedeanClassOrderIso : (Γ : Type u_1) →
  (R : Type u_2) →
    [inst : LinearOrder Γ] →
      [inst_1 : LinearOrder R] →
        [inst_2 : AddCommGroup R] →
          [inst_3 : IsOrderedAddMonoid R] →
            [Archimedean R] → [Nontrivial R] → FiniteArchimedeanClass (Lex (HahnSeries Γ R)) ≃o Γ
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instIsRightCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsRightCancelMul α], IsRightCancelMul αᵒᵈ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.eq_empty_iff_forall_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t = ∅ ↔ ∀ (a : α), t.contains a = false
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.hasColimit : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantFrom i₀ → ∀ [CategoryTheory.IsFiltered J], CategoryTheory.Limits.HasColimit F
-- Mathlib.RingTheory.Polynomial.Quotient
Polynomial.quotientSpanXSubCAlgEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] (x y : R),
  (Polynomial.quotientSpanXSubCAlgEquiv x).symm y =
    (algebraMap R (Polynomial R ⧸ Ideal.span {Polynomial.X - Polynomial.C x})) y
-- Mathlib.Order.Restriction
Preorder.frestrictLe.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] (a : α),
  Preorder.frestrictLe a = (Finset.Iic a).restrict
-- Mathlib.Tactic.Linarith.Datatypes
/-- A `Comp` represents a contradiction if its expression has no coefficients and its strength is <,
that is, it represents the fact `0 < 0`.
 -/
Mathlib.Tactic.Linarith.Comp.isContr : Mathlib.Tactic.Linarith.Comp → Bool
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instContinuousConstSMul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] (M : Type u_6) [inst_7 : Monoid M] [inst_8 : DistribMulAction M F]
  [inst_9 : SMulCommClass 𝕜₂ M F] [inst_10 : TopologicalSpace F] [inst_11 : IsTopologicalAddGroup F]
  [inst_12 : ContinuousConstSMul M F] (𝔖 : Set (Set E)), ContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖)
-- Init.Data.Option.Lemmas
Option.elim_guard : ∀ {α : Type u_1} {p : α → Bool} {a : α} {α_1 : Sort u_2} {b : α_1} {f : α → α_1},
  (Option.guard p a).elim b f = if p a = true then f a else b
-- Init.Data.List.Lemmas
List.nil_eq_append_iff : ∀ {α : Type u_1} {a b : List α}, [] = a ++ b ↔ a = [] ∧ b = []
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Context.mk.inj : ∀ {useMT : Bool} {thm : Lean.Meta.Grind.EMatchTheorem} {initApp : Lean.Expr} {useMT_1 : Bool}
  {thm_1 : Lean.Meta.Grind.EMatchTheorem} {initApp_1 : Lean.Expr},
  { useMT := useMT, thm := thm, initApp := initApp } = { useMT := useMT_1, thm := thm_1, initApp := initApp_1 } →
    useMT = useMT_1 ∧ thm = thm_1 ∧ initApp = initApp_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0π_comp_H0Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.H0π A) (groupHomology.H0Iso A).hom = (Rep.coinvariantsMk k G).app A
-- Mathlib.LinearAlgebra.Contraction
/-- If the identity linear map lies in the range of the canonical map `M* ⊗[R] M → Hom_R(M, M)`,
then `M` is a finite projective `R`-module (projective part).  -/
Module.Projective.of_one_mem_range_dualTensorHom : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  1 ∈ (dualTensorHom R M M).range → Module.Projective R M
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.FormallyUnramified (CategoryTheory.CategoryStruct.comp f g)],
  AlgebraicGeometry.FormallyUnramified f
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.isOpen_ball : ∀ {α : Type ua} [inst : UniformSpace α] (x : α) {V : SetRel α α}, IsOpen V → IsOpen (UniformSpace.ball x V)
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem:
Weak convergence of probability measures implies that if a set is clopen, then the limit of the
measures of the set equals the measure of the set under the limit probability measure.
 -/
MeasureTheory.ProbabilityMeasure.tendsto_measure_of_isClopen_of_tendsto : ∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [inst_2 : OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω}
  {μs : ι → MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs L (nhds μ) → ∀ {E : Set Ω}, IsClopen E → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry.stx : Lean.Server.FileWorker.NamespaceEntry → Lean.Syntax
-- Mathlib.Algebra.Order.Archimedean.Basic
archimedean_iff_int_le : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K],
  Archimedean K ↔ ∀ (x : K), ∃ n, x ≤ ↑n
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.det_taylorLinearEquiv : ∀ {R : Type u_1} [inst : CommRing R] {r : R} {n : ℕ}, LinearEquiv.det (Polynomial.taylorLinearEquiv r n) = 1
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.inst : ∀ {R : Type u} [inst : CommRing R], Algebra.FormallyEtale R R
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.instHomIsOverHomAsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] {f : X ⟶ Y} [inst_3 : CategoryTheory.IsIso f] [CategoryTheory.HomIsOver f S],
  CategoryTheory.HomIsOver (CategoryTheory.asIso f).hom S
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_le_toNNRat_iff : ∀ {p q : ℚ}, 0 ≤ p → (q.toNNRat ≤ p.toNNRat ↔ q ≤ p)
-- Mathlib.Algebra.Order.Hom.Submonoid
Submonoid.topOrderMonoidIso_symm_apply_coe : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Monoid α] (x : α), ↑(Submonoid.topOrderMonoidIso.symm x) = x
-- Mathlib.Algebra.BigOperators.Pi
Pi.single_induction : ∀ {ι : Type u_1} [Finite ι] [inst : DecidableEq ι] {M : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  (p : ((i : ι) → M i) → Prop) (f : (i : ι) → M i),
  p 0 → (∀ (f g : (i : ι) → M i), p f → p g → p (f + g)) → (∀ (i : ι) (m : M i), p (Pi.single i m)) → p f
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcWireFormat.v1.sizeOf_spec : sizeOf Lean.Lsp.RpcWireFormat.v1 = 1
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt.go.eq_def : ∀ {α : Type u_1} (a : List α) (a_1 : ℕ) (a_2 : List α),
  List.MergeSort.Internal.splitRevAt.go✝ a a_1 a_2 =
    match a, a_1, a_2 with
    | x :: xs, n.succ, acc => List.MergeSort.Internal.splitRevAt.go✝ xs n (x :: acc)
    | xs, x, acc => (acc, xs)
-- Mathlib.Order.Bounds.Basic
NoTopOrder.upperBounds_univ : ∀ {α : Type u_1} [inst : Preorder α] [NoTopOrder α], upperBounds Set.univ = ∅
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries_zero : ∀ (G : Type u_1) [inst : Group G], Subgroup.upperCentralSeries G 0 = ⊥
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.sub_one_pow_totient_lt_cyclotomic_eval : ∀ {n : ℕ} {q : ℝ}, 2 ≤ n → 1 < q → (q - 1) ^ n.totient < Polynomial.eval q (Polynomial.cyclotomic n ℝ)
-- Mathlib.Order.RelClasses
instIrreflOfIsNonstrictStrictOrder : ∀ {α : Type u} {r s : α → α → Prop} [IsNonstrictStrictOrder α r s], Std.Irrefl s
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological_R : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M],
  (Module.Presentation.tautological A M).R = Module.Presentation.tautological.R A M
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The isomorphism `S₁.leftHomology ≅ S₂.leftHomology` induced by an isomorphism of
short complexes `S₁ ≅ S₂`.  -/
CategoryTheory.ShortComplex.leftHomologyMapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) → [inst_2 : S₁.HasLeftHomology] → [inst_3 : S₂.HasLeftHomology] → S₁.leftHomology ≅ S₂.leftHomology
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.le_iff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  π₂.IsPartition → (π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J')
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Eta-expanded form of `MeromorphicOn.divisor_comp_sub_const_eq_divisor`

---

Divisors are invariant under translation.  -/
MeromorphicOn.divisor_fun_comp_sub_const_eq_divisor : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {f : 𝕜 → E},
  (MeromorphicOn.divisor (fun x => f (x - c)) U) (z + c) = (MeromorphicOn.divisor f (U - {c})) z
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.forget₂_map : ∀ {R S : AddGrpCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ AddGrpCat AddMonCat).obj R)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ AddGrpCat AddMonCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
map_isIntegral_int : ∀ {B : Type u_5} {C : Type u_6} {F : Type u_7} [inst : Ring B] [inst_1 : Ring C] {b : B} [inst_2 : FunLike F B C]
  [RingHomClass F B C] (f : F), IsIntegral ℤ b → IsIntegral ℤ (f b)
-- Mathlib.Order.Monotone.Monovary
antivaryOn_const_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β)
  (s : Set ι), AntivaryOn f (Function.const ι b) s
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_univ : ∀ {α : Type u_2} {r : α → α → Prop}, Set.univ.WellFoundedOn r ↔ WellFounded r
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.prod : ∀ {𝕜 : 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] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedCommRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {ι : Type} {t : Finset ι} {f : ι → M → F'}
  {f' : ι → TangentSpace I z →L[𝕜] F'} [inst_8 : DecidableEq ι],
  (∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) →
    HasMFDerivAt[s] (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)
-- Init.Data.UInt.Bitwise
UInt16.toUSize_or : ∀ (a b : UInt16), (a ||| b).toUSize = a.toUSize ||| b.toUSize
-- Lean.Environment
/-- Kernel typecheck function. We use it mainly for debugging purposes.
Recall that the Kernel type checker does not support metavariables.
When implementing automation, consider using the `MetaM` methods.  -/
Lean.Kernel.check : Lean.Environment → Lean.LocalContext → Lean.Expr → Except Lean.Kernel.Exception Lean.Expr
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
affineSpan_subset_span : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {s : Set V},
  ↑(affineSpan k s) ⊆ ↑(Submodule.span k s)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.mem_closure_iff : ∀ {α : Type u_2} {M : Matroid α} {I : Set α} {x : α}, M.Indep I → (x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I)
-- Mathlib.RingTheory.WittVector.Basic
WittVector.wittNSMul.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), WittVector.wittNSMul p n = wittStructureInt p (n • MvPolynomial.X 0)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The relations in the standard presentation of `⋀[R]^n M` with generators and relations.  -/
exteriorPower.presentation.relations : (R : Type u) →
  [inst : CommRing R] →
    (ι : Type u_4) → [DecidableEq ι] → (M : Type u_5) → [inst_2 : AddCommGroup M] → [Module R M] → Module.Relations R
-- Mathlib.Order.CompleteLattice.Basic
iSup_plift_down : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] (f : ι → α), ⨆ i, f i.down = ⨆ i, f i
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_toList_insert_of_mem : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v' : α} (v : α) {t : RBTree.RBSet α cmp},
  v' ∈ t.toList → v' ∈ (t.insert v).toList ∨ cmp v v' = Ordering.eq
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C]
  {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl)
        (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr))
      (CategoryTheory.Limits.codiag (Y ⨿ Y')) =
    CategoryTheory.Limits.coprod.map g g'
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f pf s x → HasFPowerSeriesWithinAt g pg s x → HasFPowerSeriesWithinAt (f - g) (pf - pg) s x
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instR1Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [R1Space M], R1Space Mᵈᵐᵃ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α},
  t.WF →
    (Array.find? (fun x => compare x.1 k == Ordering.eq) (Std.DTreeMap.Internal.Impl.Const.toArray t) = none ↔
      Std.DTreeMap.Internal.Impl.contains k t = false)
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenexImpRight.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4)
  (n : ℕ) (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α (n + 1))
  (h_1 :
    (n : ℕ) →
      (φ : L.BoundedFormula α n) →
        (ψ : L.BoundedFormula α (n + 1)) →
          motive n φ
            ((ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum))
  (h_2 : (n : ℕ) → (φ : L.BoundedFormula α n) → (ψ : L.BoundedFormula α (n + 1)) → motive n φ ψ.all)
  (h_3 : (_n : ℕ) → (φ ψ : L.BoundedFormula α _n) → motive _n φ ψ),
  (match n, φ, (ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum with
    | n, φ, (ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum =>
      h_1 n φ ψ
    | n, φ, ψ.all => h_2 n φ ψ
    | _n, φ, ψ => h_3 _n φ ψ) =
    h_1 n φ ψ
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial.eq_1 : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂),
  LinearMap.toMvPolynomial b₁ b₂ f i = ((LinearMap.toMatrix b₁ b₂) f).toMvPolynomial i
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.val_addUnit' : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α} (h : IsAddUnit a), ↑h.addUnit' = a
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.instInhabitedCharRole : Inhabited Lean.FuzzyMatching.CharRole