mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C),
  groupHomology.chainsMap (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap f φ) (groupHomology.chainsMap g ψ)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.unit_naturality_assoc : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) ⦃X Y : C⦄ (f : X ⟶ Y) {Z : C}
  (h : T.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (T.η.app Y) h) =
    CategoryTheory.CategoryStruct.comp (T.η.app X) (CategoryTheory.CategoryStruct.comp (T.map f) h)
-- Init.Data.SInt.Basic
instComplementInt32 : Complement Int32
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed : ∀ {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} [Countable ι] (f : MeasureTheory.SimpleFunc α ENNReal)
  {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s →
    ∀ (μ : MeasureTheory.Measure α), f.lintegral (μ.restrict (⋃ i, s i)) = ⨆ i, f.lintegral (μ.restrict (s i))
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_inf : ∀ {G : Type u_1} [inst : AddGroup G] {p p' : AddSubgroup G} {x : G}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.mk : ∀ {R : Type v} {A : Type u} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Subsingleton Ω[A⁄R] → Algebra.FormallyUnramified R A
-- Mathlib.Order.RelClasses
instIsWellFoundedInvImageNatLt : ∀ {α : Type u} (f : α → ℕ), IsWellFounded α (InvImage (fun x1 x2 => x1 < x2) f)
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.orderOf_one_add_prime : ∀ {p : ℕ}, Nat.Prime p → p ≠ 2 → ∀ (n : ℕ), orderOf (1 + ↑p) = p ^ n
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatISizeSintNumBits : Lean.Grind.ToInt.OfNat ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
-- Mathlib.Algebra.Module.Torsion.Free
/-- Only a ring of characteristic zero can have a non-trivial module without additive or
scalar torsion.  -/
CharZero.of_isAddTorsionFree : ∀ (R : Type u_1) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommGroup M] [Module R M] [Nontrivial M]
  [IsAddTorsionFree M], CharZero R
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.moebius_mul_log_eq_vonMangoldt : ↑ArithmeticFunction.moebius * ArithmeticFunction.log = ArithmeticFunction.vonMangoldt
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- The prime spectrum of a commutative (semi)ring is a compact topological space.  -/
PrimeSpectrum.compactSpace : ∀ {R : Type u} [inst : CommSemiring R], CompactSpace (PrimeSpectrum R)
-- Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
CategoryTheory.MonoidalCategory.Limits.HasColimit.isoOfNatIso_ι_hom_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {J : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {F G : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] [inst_4 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J)
  {Q : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.ι F j) Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom Q) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (w.hom.app j) Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.colimit.ι G j) Q)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.deriv_lt_ord : ∀ {f : Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}},
  c.IsRegular →
    c ≠ Cardinal.aleph0 → (∀ i < c.ord, f i < c.ord) → ∀ {a : Ordinal.{u}}, a < c.ord → Ordinal.deriv f a < c.ord
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ),
  ‖p.changeOriginSeries k l‖₊ ≤ ∑' (x : { s // s.card = l }), ‖p (k + l)‖₊
-- Init.Data.Nat.Log2
Nat.log2.eq_1 : ∀ (n : ℕ),
  n.log2 =
    Nat.rec (motive := fun x => ℕ → ℕ) (fun x => 0) (fun x ih n => Bool.rec 0 (ih (n.div 2)).succ (Nat.ble 2 n)) n n
-- Lean.Elab.DocString
/-- The monad in which documentation is elaborated.
 -/
Lean.Doc.DocM : Type → Type
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductCocone_pt : ∀ (X Y : Type u), (CategoryTheory.Limits.Types.binaryCoproductCocone X Y).pt = (X ⊕ Y)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions are preserved under 2-Freiman isos.  -/
IsAddFreimanIso.addRothNumber_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β]
  [inst_3 : DecidableEq β] {A : Finset α} {B : Finset β} {f : α → β},
  IsAddFreimanIso 2 (↑A) (↑B) f → addRothNumber A = addRothNumber B
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.isStarNormal : ∀ {R : Type u_1} {p : R} [inst : Mul R] [inst_1 : Star R], IsStarProjection p → IsStarNormal p
-- Mathlib.Control.Functor.Multivariate
/-- laws for `MvFunctor`  -/
LawfulMvFunctor : {n : ℕ} → (F : TypeVec.{u_2} n → Type u_1) → [MvFunctor F] → Prop
-- Mathlib.GroupTheory.Focal
/-- Lemma: H* is a normal subgroup of H.  -/
AddSubgroup.instNormalSubtypeMemFocalAddSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.focalAddSubgroupOf.Normal
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.sr : {n : ℕ} → ZMod n → DihedralGroup n
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.id_apply : ∀ (R : SemiRingCat) (r : ↑R), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id R)) r = r
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.FunInfoEnvCacheKey.maxArgs? : Lean.Meta.FunInfoEnvCacheKey✝ → Option ℕ
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.IsAffineOpen.preimage : ∀ {X Y : AlgebraicGeometry.Scheme} {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f],
      AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_slice : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : String.Pos.Raw),
  String.Pos.Raw.IsValidForSlice (s.slice p₀ p₁ h) pos ↔
    pos.offsetBy p₀.offset ≤ p₁.offset ∧ String.Pos.Raw.IsValidForSlice s (pos.offsetBy p₀.offset)
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.trivialization_apply : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (a : Bundle.TotalSpace F (Bundle.Trivial B F)), ↑(Bundle.Trivial.trivialization B F) a = (a.proj, a.snd)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, m.contains a = true ↔ a ∈ m
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- The second exterior derivative of a sufficiently smooth differential form is zero.  -/
extDerivWithin_extDerivWithin_eqOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {r : WithTop ℕ∞}
  {ω : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E},
  ContDiffOn 𝕜 r ω s →
    minSmoothness 𝕜 2 ≤ r →
      UniqueDiffOn 𝕜 s → Set.EqOn (extDerivWithin (extDerivWithin ω s) s) 0 (s ∩ closure (interior s))
-- Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Function.locallyFinsuppWithin.restrictMonoidHom.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y] {V : Set X}
  (h : V ⊆ U),
  Function.locallyFinsuppWithin.restrictMonoidHom h = { toFun := fun D => D.restrict h, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Computability.Reduce
/-- `p` is one-one reducible to `q` if there is an injective computable function translating questions
about `p` to questions about `q`.
 -/
OneOneReducible : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → (α → Prop) → (β → Prop) → Prop
-- Mathlib.CategoryTheory.Action.Limits
Action.instReflectsColimitsOfShapeForget : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J], CategoryTheory.Limits.ReflectsColimitsOfShape J (Action.forget V G)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_le_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k t = true → (compare t.minKey! k).isLE = true
-- Init.Data.Vector.Basic
/-- Compares two vectors of the same size using a given boolean relation `r`. `isEqv v w r` returns
`true` if and only if `r v[i] w[i]` is true for all indices `i`.
 -/
Vector.isEqv : {α : Type u_1} → {n : ℕ} → Vector α n → Vector α n → (α → α → Bool) → Bool
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits
SheafOfModules.instHasColimitsOfShapeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [J.WEqualsLocallyBijective AddCommGrpCat] (K : Type w) [inst_3 : CategoryTheory.Category.{w', w} K]
  [CategoryTheory.Limits.HasColimitsOfShape K (PresheafOfModules R.obj)],
  CategoryTheory.Limits.HasColimitsOfShape K (SheafOfModules R)
-- Mathlib.Topology.Algebra.Group.Defs
IsTopologicalGroup.mk : ∀ {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : Group G] [toContinuousMul : ContinuousMul G]
  [toContinuousInv : ContinuousInv G], IsTopologicalGroup G
-- Lean.Meta.ArgsPacker
/-- Iterated `PSum.casesOn`:
Given a value `(x : A ⊕ C)` (which must be a FVar) and functions
`alt₁ : (a : A) → codomain[inl a]` and `alt₂ : (b : B) → codomain[inr b]`,
matches on `x` to apply the right `alt` to produce a value of `codomain[x]`.

Uses the variable name from the lambda in `altᵢ`, if present.
 -/
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Mutual.casesOn : Lean.Expr → Lean.Expr → List Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.UpperLower.Basic
isLowerSet_univ : ∀ {α : Type u_1} [inst : LE α], IsLowerSet Set.univ
-- Mathlib.Data.Set.Basic
Set.union_subset_union : ∀ {α : Type u} {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ∪ t₁ ⊆ s₂ ∪ t₂
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.oset.congr_simp : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  fvarId = fvarId_1 →
    ∀ (i i_1 : ℕ),
      i = i_1 →
        ∀ (y y_1 : Lean.Compiler.LCNF.Arg pu),
          y = y_1 →
            ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
              k = k_1 →
                ∀ (h : pu = Lean.Compiler.LCNF.Purity.impure),
                  Lean.Compiler.LCNF.Code.oset fvarId i y k h = Lean.Compiler.LCNF.Code.oset fvarId_1 i_1 y_1 k_1 h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : β k → β k} {fallback : α}, (t.modify k f).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Data.Set.Card.Arithmetic
Set.exists_union_disjoint_cardinal_eq_of_even : ∀ {α : Type u_1} {s : Set α}, Even s.ncard → ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk ↑t = Cardinal.mk ↑u
-- Mathlib.Data.List.Sym
List.sym.eq_3 : ∀ {α : Type u_1} (n : ℕ) (x_2 : α) (xs : List α),
  List.sym n.succ (x_2 :: xs) = List.map (fun p => x_2 ::ₛ p) (List.sym n (x_2 :: xs)) ++ List.sym (n + 1) xs
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_l : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] {X Y : C} (f : X ⟶ Y)
  (hf : W f) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.ιLeft f hf g)
      (CategoryTheory.OrthogonalReflection.D₁.l W Z) =
    g
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMotivesPi : Lean.Options → Bool
-- Mathlib.Order.Basic
/-- A function `a` is strongly less than a function `b` if `a i < b i` for all `i`.  -/
StrongLT : {ι : Type u_1} → {π : ι → Type u_4} → [(i : ι) → LT (π i)] → ((i : ι) → π i) → ((i : ι) → π i) → Prop
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.instDecidableEqOffset.decEq : (x x_1 : Std.Time.TimeZone.Offset) → Decidable (x = x_1)
-- Lean.Compiler.ExternAttr
Lean.instBEqExternAttrData.beq : Lean.ExternAttrData → Lean.ExternAttrData → Bool
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The bialgebra equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of
`Additive`.  -/
MonoidAlgebra.toAdditiveBialgEquiv : (R : Type u_1) →
  (A : Type u_3) →
    (M : Type u_8) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Bialgebra R A] → [inst_3 : Monoid M] → MonoidAlgebra A M ≃ₐc[R] AddMonoidAlgebra A (Additive M)
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.step_take.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α]
  (aig : Std.Sat.AIG α) (wn wr : ℕ) (q r : aig.RefVec w) (hle : old.decls.size ≤ aig.decls.size),
  sizeOf { aig := aig, wn := wn, wr := wr, q := q, r := r, hle := hle } =
    1 + sizeOf aig + sizeOf wn + sizeOf wr + sizeOf q + sizeOf r + sizeOf hle
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_add : ∀ {α : Type u_3} [inst : Monoid α] (s t : Multiset α) (comm : {x | x ∈ s + t}.Pairwise Commute),
  (s + t).noncommProd comm = s.noncommProd ⋯ * t.noncommProd ⋯
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.absolutelyContinuous_cond_univ : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  μ.AbsolutelyContinuous μ[|Set.univ]
-- Mathlib.Logic.Equiv.Basic
/-- A helper function for `Equiv.swap`.  -/
Equiv.swapCore : {α : Sort u_1} → [DecidableEq α] → α → α → α → α
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.isPeriodicPt_vadd_iff : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α} {n : ℕ},
  Function.IsPeriodicPt (fun x => m +ᵥ x) n a ↔ n • m +ᵥ a = a
-- Init.Data.SInt.Lemmas
Int32.ofInt_eq_iff_bmod_eq_toInt : ∀ (a : ℤ) (b : Int32), Int32.ofInt a = b ↔ a.bmod (2 ^ 32) = b.toInt
-- Mathlib.Analysis.Convex.Basic
Convex.translate : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 ((fun x => z + x) '' s)
-- Std.Data.DHashMap.Raw
/-- Removes all mappings of the hash map for which the given function returns `false`.  -/
Std.DHashMap.Raw.filter : {α : Type u} → {β : α → Type v} → ((a : α) → β a → Bool) → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetInstance.mk : Lean.Widget.WidgetInstance → Option Lean.Lsp.Range → Option String → Lean.Widget.PanelWidgetInstance
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If `f₁` is meromorphic on `U`, if `f₂` agrees with `f₁` on a codiscrete subset of `U` and outside of
`U`, then `f₁` and `f₂` induce the same divisors on `U`.
 -/
MeromorphicOn.divisor_congr_codiscreteWithin_of_eqOn_compl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E},
  MeromorphicOn f₁ U →
    f₁ =ᶠ[Filter.codiscreteWithin U] f₂ → Set.EqOn f₁ f₂ Uᶜ → MeromorphicOn.divisor f₁ U = MeromorphicOn.divisor f₂ U
-- Mathlib.FieldTheory.Separable
Polynomial.separable_prod' : ∀ {R : Type u} [inst : CommRing R] {ι : Type u_1} {f : ι → Polynomial R} {s : Finset ι},
  (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
-- Mathlib.Algebra.Order.Hom.Ring
/-- Reinterpret an ordered ring isomorphism as an order isomorphism.  -/
OrderRingIso.toOrderIso : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Mul α] →
      [inst_1 : Add α] → [inst_2 : LE α] → [inst_3 : Mul β] → [inst_4 : Add β] → [inst_5 : LE β] → α ≃+*o β → α ≃o β
-- Init.Data.Array.Lemmas
Array.prod_empty : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α], #[].prod = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.instIsStableUnderRetractsCofibrations : (HomotopicalAlgebra.cofibrations SSet).IsStableUnderRetracts
-- Lean.Meta.Tactic.Util
Lean.Meta.mkFreshExprSyntheticOpaqueMVar : Lean.Expr → optParam Lean.Name Lean.Name.anonymous → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.WittVector.Domain
WittVector.verschiebung_nonzero : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] {x : WittVector p R},
  x ≠ 0 → ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑WittVector.verschiebung)^[n] x'
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity holds if and only if all extended distances between points with different
indices are proportional.  -/
similar_iff_exists_pairwise_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ico_add_one_right_eq_Icc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α),
  Set.Ico a (b + 1) = Set.Icc a b
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_Ioo_natAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m ⁻¹' Set.Ioo (Fin.natAdd m i) (Fin.natAdd m j) = Set.Ioo i j
-- Std.Sync.Notify
Std.Notify.mk.sizeOf_spec : ∀ (state : Std.Mutex Std.Notify.State), sizeOf { state := state } = 1 + sizeOf state
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnostics.mk : Lean.Lsp.WaitForDiagnostics
-- Mathlib.Algebra.Notation.Indicator
Set.mem_range_indicator : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {r : M} {s : Set α} {f : α → M},
  r ∈ Set.range (s.indicator f) ↔ r = 0 ∧ s ≠ Set.univ ∨ r ∈ f '' s
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- An isomorphism in `SimplexCategory` induces an `OrderIso`.  -/
SimplexCategory.orderIsoOfIso : {x y : SimplexCategory} → (x ≅ y) → Fin (x.len + 1) ≃o Fin (y.len + 1)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'_of_not_terminates : ∀ {α : Type u} {s : Stream'.Seq α}, ¬s.Terminates → s.length' = ⊤
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of an `AddCommMonoid` by an additive congruence
relation is an `AddCommMonoid`.  -/
AddCon.addCommMonoid : {M : Type u_4} → [inst : AddCommMonoid M] → (c : AddCon M) → AddCommMonoid c.Quotient
-- Mathlib.Analysis.InnerProductSpace.Calculus
fderivInnerCLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] (p x : E × E), (fderivInnerCLM 𝕜 p) x = inner 𝕜 p.1 x.2 + inner 𝕜 x.1 p.2
-- Mathlib.Tactic.NormNum.GCD
/-- Given two integers, return their GCD and an equality proof.
Panics if `ex` or `ey` aren't integer literals.  -/
Mathlib.Meta.NormNum.proveIntGCD : (ex ey : Q(ℤ)) → (ed : Q(ℕ)) × Q(«$ex».gcd «$ey» = «$ed»)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.MonadShareCommon : (Type → Type) → Type
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Cat} (F : X ⟶ Y)
  (X_1 : CategoryTheory.Join C ↑X),
  ((CategoryTheory.Join.pseudofunctorRight C).map F).toFunctor.obj X_1 =
    match X_1 with
    | CategoryTheory.Join.left x => CategoryTheory.Join.left x
    | CategoryTheory.Join.right x => CategoryTheory.Join.right (F.toFunctor.obj x)
-- Mathlib.Order.Atoms
eq_iff_atom_le_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] [IsAtomistic α] {a b : α},
  a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Entries.mk : Lean.ExprMap Mathlib.Explode.Entry → List Mathlib.Explode.Entry → Mathlib.Explode.Entries
-- Mathlib.Data.Countable.Basic
Option.instUncountable : ∀ {α : Type u} [Uncountable α], Uncountable (Option α)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_piCongrLeft : ∀ {δ : Type u_4} {δ' : Type u_5} {π : δ' → Type u_6} [inst : (x : δ') → MeasurableSpace (π x)] (f : δ ≃ δ'),
  ⇑(MeasurableEquiv.piCongrLeft π f) = ⇑(Equiv.piCongrLeft π f)
-- Mathlib.Analysis.Normed.Operator.Basic
/-- The fundamental property of the operator norm: `‖f x‖ ≤ ‖f‖ * ‖x‖`.  -/
ContinuousLinearMap.le_opNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  (x : E), ‖f x‖ ≤ ‖f‖ * ‖x‖
-- Mathlib.Topology.Instances.Complex
Subfield.toIntermediateField.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S S_1 : Subfield L)
  (e_S : S = S_1) (algebra_map_mem : ∀ (x : K), (algebraMap K L) x ∈ S),
  S.toIntermediateField algebra_map_mem = S_1.toIntermediateField ⋯
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_add_smul_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} {c : ι → R} {i : ι}, c i = 0 → (LinearIndependent R (v + fun x => c x • v i) ↔ LinearIndependent R v)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.size.eq_2 : ∀ {α : Type u_1} (sz : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α), (Ordnode.node sz l x_1 r).size = sz
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.measure_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb → ∀ {s : Set β}, MeasureTheory.NullMeasurableSet s μb → μa (f ⁻¹' s) = μb s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_of_beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap α (fun x => β) cmp} [inst : BEq β]
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [LawfulBEq β], Std.DTreeMap.Const.beq m₁ m₂ = true → m₁.Equiv m₂
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G × G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A)) fun₀ | g => a) =
    ((fun₀ | g.2 => (A.ρ g.1⁻¹) a) - fun₀ | g.1 * g.2 => a) + fun₀ | g.1 => a