mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- If `p` is a maximal ideal of `R`, `S` extends `R` and `P^e` lies over `p`,
then the dimension `[S/(P^e) : R/p]` is equal to `e * [S/P : R/p]`.  -/
Ideal.rank_prime_pow_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime],
  P ≠ ⊥ →
    ∀ (he : p.ramificationIdx' P ≠ 0),
      Module.rank (R ⧸ p) (S ⧸ P ^ p.ramificationIdx' P) = p.ramificationIdx' P • Module.rank (R ⧸ p) (S ⧸ P)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mulPosReflectLE_iff_mulPosReflectLT : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : PartialOrder α] [IsRightCancelMulZero α],
  MulPosReflectLE α ↔ MulPosReflectLT α
-- Mathlib.Tactic.ClearExclamation
/-- A variant of `clear` which clears not only the given hypotheses but also any other hypotheses
depending on them  -/
Mathlib.Tactic.clear! : Lean.ParserDescr
-- Mathlib.Order.WellFounded
/-- A minimal element of a nonempty set in a well-founded order.

If you're working with a nonempty linear order, consider defining a
`ConditionallyCompleteLinearOrderBot` instance via
`WellFoundedLT.conditionallyCompleteLinearOrderBot` and using `Inf` instead.  -/
WellFounded.min : {α : Type u_1} → {r : α → α → Prop} → WellFounded r → (s : Set α) → s.Nonempty → α
-- Mathlib.Algebra.Homology.Augment
CochainComplex.augmentTruncate_inv_f_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) (i : ℕ), C.augmentTruncate.inv.f (i + 1) = CategoryTheory.CategoryStruct.id (C.X (i + 1))
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.instIsSplitMonoLeftIArrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : Y ⟶ X} {g : W ⟶ Z}
  (h : CategoryTheory.RetractArrow f g), CategoryTheory.IsSplitMono (CategoryTheory.Arrow.Hom.left h.i)
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.instCategory : (A : Type u_1) → CategoryTheory.Category.{0, u_1} (CategoryTheory.Codiscrete A)
-- Mathlib.Order.Category.Semilat
/-- Constructs an isomorphism of lattices from an order isomorphism between them.  -/
SemilatSupCat.Iso.mk : {α β : SemilatSupCat} → α.X ≃o β.X → (α ≅ β)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.all_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {p : (a : α) → β a → Bool},
  (↑m).WF → ((↑m).all p = false ↔ ∃ a, ∃ (h : m.contains a = true), p a (m.get a h) = false)
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
/-- Converting a bundled algebra to a monoid object in `ModuleCat R`.
 -/
ModuleCat.MonModuleEquivalenceAlgebra.inverse : {R : Type u} → [inst : CommRing R] → CategoryTheory.Functor (AlgCat R) (CategoryTheory.Mon (ModuleCat R))
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.SummableFamily.binomialFamily_orderTop_pos : ∀ {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : BinomialRing R] [inst_5 : CommRing A]
  [inst_6 : Algebra R A] {x : HahnSeries Γ A},
  0 < (x - 1).orderTop → ∀ (r : R) {n : ℕ}, 0 < n → 0 < ((HahnSeries.SummableFamily.binomialFamily x r) n).orderTop
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_neg_I : IsPrimitiveRoot (-Complex.I) 4
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : β → β},
  m.WF → (Std.DHashMap.Raw.Const.modify m k f).getKey? k = if k ∈ m then some k else none
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.mul_conjTranspose_self : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype m] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R),
  (Function.Injective fun v => Matrix.vecMul v A) → (A * A.conjTranspose).PosDef
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiff.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3} [inst_1 : TopologicalSpace H]
  {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M]
  {g : M → G}, ContMDiff I' I n g → ∀ (m : ℕ), ContMDiff I' I n fun x => g x ^ m
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S.eq_def : ∀ (R : Type u_1) [inst : CommRing R] (x : ℤ),
  Polynomial.Chebyshev.S R x =
    match x with
    | 0 => 1
    | 1 => Polynomial.X
    | Int.ofNat n.succ.succ => Polynomial.X * Polynomial.Chebyshev.S R (↑n + 1) - Polynomial.Chebyshev.S R ↑n
    | Int.negSucc n => Polynomial.X * Polynomial.Chebyshev.S R (-↑n) - Polynomial.Chebyshev.S R (-↑n + 1)
-- Mathlib.Data.Sym.Basic
Sym.coe_inj : ∀ {α : Type u_1} {n : ℕ} {s₁ s₂ : Sym α n}, ↑s₁ = ↑s₂ ↔ s₁ = s₂
-- Mathlib.Logic.Basic
/-- **Alias** of `Classical.and_or_imp`. -/
and_or_imp : ∀ {a b c : Prop}, a ∧ b ∨ (a → c) ↔ a → b ∨ c
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.CommShift.mk : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {adj : F ⊣ G} {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A],
  autoParam (CategoryTheory.NatTrans.CommShift adj.unit A)
      CategoryTheory.Adjunction.CommShift.commShift_unit._autoParam →
    autoParam (CategoryTheory.NatTrans.CommShift adj.counit A)
        CategoryTheory.Adjunction.CommShift.commShift_counit._autoParam →
      adj.CommShift A
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toArray_ensureTermination_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} {it : Std.IterM m β} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Std.Iterator α m β] [inst_3 : Std.Iterators.Finite α m],
  it.ensureTermination.toArray = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.toArray
        pure (#[out] ++ __do_lift)
      | Std.IterStep.skip it' => it'.toArray
      | Std.IterStep.done => pure #[]
-- Std.Data.TreeSet.Raw.DecidableEquiv
Std.TreeSet.Raw.instDecidableEquiv : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] →
      [Std.LawfulEqCmp cmp] → {t₁ t₂ : Std.TreeSet.Raw α cmp} → t₁.WF → t₂.WF → Decidable (t₁.Equiv t₂)
-- Mathlib.Topology.Algebra.Module.Complement
/-- If `p` and `q` are topological complements and `q` is Hausdorff, then `p` is closed.  -/
Submodule.IsTopCompl.isClosed : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [T1Space ↥q] [ContinuousSub M], Submodule.IsTopCompl p q → IsClosed ↑p
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.mapsTo_extend : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M},
  s ⊆ f.source → Set.MapsTo (↑(f.extend I)) s (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)
-- Mathlib.LinearAlgebra.Matrix.ToLin
range_vecMulLinear : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m] (M : Matrix m n R),
  M.vecMulLinear.range = Submodule.span R (Set.range M.row)
-- Mathlib.Data.List.Basic
List.getLast?_append_of_ne_nil : ∀ {α : Type u} (l₁ : List α) {l₂ : List α}, l₂ ≠ [] → (l₁ ++ l₂).getLast? = l₂.getLast?
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- A well-founded relation on `R`, satisfying `r (a % b) b`.
This ensures that the GCD algorithm always terminates.  -/
EuclideanDomain.r : {R : Type u} → [self : EuclideanDomain R] → R → R → Prop
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β], UniformFun.toFun 0 = 0
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.bot_mem_precoverage : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (X : AlgebraicGeometry.Scheme) [IsEmpty ↥X],
  ⊥ ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X
-- Mathlib.SetTheory.Lists
Lists'.ofList.eq_1 : ∀ {α : Type u_1}, Lists'.ofList [] = Lists'.nil
-- Mathlib.Tactic.CongrExclamation
/-- Like `Lean.MVarId.congr?` but instead of using only the congruence lemma associated to the LHS,
it tries the RHS too, in the order specified by `config.preferLHS`.

It uses `Lean.Meta.mkCongrSimp?` to generate a congruence lemma, like in the `congr` tactic.

Applies the congruence generated congruence lemmas according to `config`.
 -/
Lean.MVarId.congrSimp? : Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Data.List.DropRight
List.rdropWhile_append_rtakeWhile : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.rdropWhile p l ++ List.rtakeWhile p l = l
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.whiskerRight_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ : CategoryTheory.Center C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Center C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y).f =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.f Y.fst
-- Mathlib.Topology.NhdsWithin
nhds_of_nhdsWithin_of_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {a : α}, s ∈ nhds a → t ∈ nhdsWithin a s → t ∈ nhds a
-- Mathlib.FieldTheory.RatFunc.Valuation
/-- The valuation at infinity on `k(t)` extends to a valuation on `CompletionAtInfty`.  -/
RatFunc.CompletionAtInfty.instValuedWithZeroMultiplicativeInt : (F : Type u_1) →
  [inst : Field F] →
    [inst_1 : DecidableEq (RatFunc F)] → Valued (RatFunc.CompletionAtInfty F) (WithZero (Multiplicative ℤ))
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- The canonical factor `CanonicalFactor R w` is analytic on the complement of `w`.
 -/
Complex.analyticOnNhd_canonicalFactor : ∀ (R : ℝ) (w : ℂ), AnalyticOnNhd ℂ (Complex.canonicalFactor R w) {w}ᶜ
-- Init.Data.Vector.Lex
Vector.not_lt : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n}, ¬xs < ys ↔ ys ≤ xs
-- Mathlib.Data.Nat.MaxPowDiv
/-- If `p > 1`, `n > 0`, then the first component of `maxPowDvdDiv` is the maximal power of `p`
that divides `n`.  -/
Nat.pow_dvd_iff_le_padicValNat : ∀ {p k n : ℕ}, p ≠ 1 → n ≠ 0 → (p ^ k ∣ n ↔ k ≤ padicValNat p n)
-- Mathlib.Topology.Order.OrderClosed
closure_Icc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] (a b : α),
  closure (Set.Icc a b) = Set.Icc a b
-- Mathlib.Data.ENat.Basic
ENat.natCast_sub : ∀ (m n : ℕ), ↑(m - n) = ↑m - ↑n
-- Mathlib.Data.Fin.SuccPred
Fin.succ_natAdd : ∀ {n m : ℕ} (i : Fin m), (Fin.natAdd n i).succ = Fin.natAdd n i.succ
-- Mathlib.RingTheory.Polynomial.IsIntegral
/-- [Stacks Tag 00H0](https://stacks.math.columbia.edu/tag/00H0) ((1)) -/
IsAlmostIntegral.coeff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [FaithfulSMul R S] {p : Polynomial S}, IsAlmostIntegral (Polynomial R) p → ∀ (i : ℕ), IsAlmostIntegral R (p.coeff i)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.pi_top : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] (I : Set ι),
  (AddSubmonoid.pi I fun i => ⊤) = ⊤
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, (t.erase k).getD k fallback = fallback
-- Mathlib.GroupTheory.Finiteness
Subgroup.FG.sup : ∀ {G : Type u_3} [inst : Group G] {P Q : Subgroup G}, P.FG → Q.FG → (P ⊔ Q).FG
-- Mathlib.MeasureTheory.Group.GeometryOfNumbers
/-- The **Minkowski Convex Body Theorem for compact domain**. If `s` is a convex compact symmetric
domain of `E` whose volume is large enough compared to the covolume of a lattice `L` of `E`, then it
contains a non-zero lattice point of `L`. Compared to
`exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure`, this version requires in addition
that `s` is compact and `L` is discrete but provides a weaker inequality rather than a strict
inequality.  -/
MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [Nontrivial E] [μ.IsAddHaarMeasure]
  {L : AddSubgroup E} [Countable ↥L] [DiscreteTopology ↥L],
  MeasureTheory.IsAddFundamentalDomain (↥L) F μ →
    (∀ x ∈ s, -x ∈ s) → Convex ℝ s → IsCompact s → μ F * 2 ^ Module.finrank ℝ E ≤ μ s → ∃ x, x ≠ 0 ∧ ↑x ∈ s
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- The image of the filter `atTop` on `Ioi a` under the coercion equals `atTop`.  -/
Filter.map_val_Ioi_atTop : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] [NoMaxOrder α] (a : α),
  Filter.map Subtype.val Filter.atTop = Filter.atTop
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
one_add_norm_le_sqrt_two_mul_sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (x : E), 1 + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)
-- Mathlib.Topology.Path
Path.trans_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b c : X} (γ₁ : Path a b) (γ₂ : Path b c),
  Set.range ⇑(γ₁.trans γ₂) = Set.range ⇑γ₁ ∪ Set.range ⇑γ₂
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRight_map_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) {Y X : CategoryTheory.Comma L R₂} (f : Y ⟶ X),
  ((CategoryTheory.Comma.mapRight L r).map f).left = f.left
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.trivializationOfVAddDisjoint_source : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hf : Topology.IsQuotientMap f) [inst_4 : ContinuousConstVAdd G E]
  (hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) [inst_5 : TopologicalSpace G]
  [inst_6 : DiscreteTopology G] (U : Set E) (open_U : IsOpen U)
  (disjoint : ∀ (g : G), ((fun x => g +ᵥ x) '' U ∩ U).Nonempty → g = 0),
  (hf.trivializationOfVAddDisjoint hfG U open_U disjoint).source = f ⁻¹' f '' U
-- Mathlib.Algebra.Order.Group.Synonym
toLex_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β), toLex (a ^ b) = toLex a ^ b
-- Mathlib.Algebra.GCDMonoid.Basic
/-- The product of two elements is `Associated` with the product of their GCD and LCM.  -/
GCDMonoid.gcd_mul_lcm : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : GCDMonoid α] (a b : α), Associated (gcd a b * lcm a b) (a * b)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasureTheory.Measure.domSMul_apply : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : MulAction G A] [inst_2 : MeasurableSpace A]
  [inst_3 : MeasurableConstSMul G A] (μ : MeasureTheory.Measure A) (g : Gᵈᵐᵃ) (s : Set A),
  (g • μ) s = μ (DomMulAct.mk.symm g • s)
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_of_ge : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), w ≤ i → x[i]? = none
-- Mathlib.Util.CompileInductive
/-- Generate compiled code for the recursor for `iv`.
 -/
Mathlib.Util.compileInductive : Lean.InductiveVal → optParam Bool true → Lean.MetaM Unit
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData S hkf hcc fac).p =
    CategoryTheory.Limits.Cofork.π cc
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.pow_eq_one_iff'' : ∀ {β : Type u_3} [Finite β] {f : Equiv.Perm β}, f.IsCycle → ∀ {n : ℕ}, f ^ n = 1 ↔ ∀ (x : β), f x ≠ x → (f ^ n) x = x
-- Mathlib.GroupTheory.GroupAction.Defs
_private.Mathlib.GroupTheory.GroupAction.Defs.0.MulAction.termΩ : Lean.ParserDescr
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_next_startPos : ∀ {s : String.Slice} {h : s.startPos ≠ s.endPos},
  (s.startPos.next h).Splits (String.singleton (s.startPos.get h)) (s.sliceFrom (s.startPos.next h)).copy
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.congr_eq_2 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (x : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none),
  x = some none →
    (match x with
      | some (some c) => h_1 c
      | some none => h_2 ()
      | none => h_3 ()) ≍
      h_2 ()
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.toAddSubmonoid_restrictScalars : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (V : Submodule R M),
  (Submodule.restrictScalars S V).toAddSubmonoid = V.toAddSubmonoid
-- Init.Data.String.Lemmas.Iterate
String.Model.revPositionsFrom_eq_map : ∀ {s : String} {p : s.Pos},
  String.Model.revPositionsFrom p =
    List.map (fun p => ⟨String.Pos.ofToSlice ↑p, ⋯⟩) (String.Slice.Model.revPositionsFrom p.toSlice)
-- Init.Grind.Norm
Lean.Grind.imp_self_eq : ∀ (p : Prop), (p → p) = True
-- Init.Data.List.Basic
List.instDecidableRelSubsetOfDecidableEq : {α : Type u} → [DecidableEq α] → DecidableRel Subset
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.all_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.copy.all pat = s.all pat
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_one_one_charP : ∀ (R : Type u_1) [inst : CommRing R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p],
  Polynomial.dickson 1 1 p = Polynomial.X ^ p
-- Mathlib.Algebra.Group.Defs
AddSemigroup.mk : {G : Type u} → [toAdd : Add G] → (∀ (a b c : G), a + b + c = a + (b + c)) → AddSemigroup G
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bfamilyOfFamily'.eq_1 : ∀ {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → α) (a : Ordinal.{u})
  (ha : a < Ordinal.type r), Ordinal.bfamilyOfFamily' r f a ha = f ((Ordinal.enum r) ⟨a, ha⟩)
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_neg : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R),
  WittVector.truncateFun n (-x) = -WittVector.truncateFun n x
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.mk : Lean.Elab.ElabInfo →
  Lean.MetavarContext → List Lean.MVarId → Lean.MetavarContext → List Lean.MVarId → Lean.Elab.TacticInfo
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- If a function `f : α → ℝ≥0` is measurable and the measure is σ-finite, then there exists
spanning measurable sets with finite measure on which `f` is bounded.
See also `StronglyMeasurable.exists_spanning_measurableSet_norm_le` for functions into normed
groups.  -/
exists_spanning_measurableSet_le : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal},
  Measurable f →
    ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
      ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, f x ≤ ↑n) ∧ ⋃ i, s i = Set.univ
-- Mathlib.Order.Filter.Extr
IsMinOn.on_subset : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
  IsMinOn f t a → s ⊆ t → IsMinOn f s a
-- Std.Time.Zoned.RecurringRule
/-- Time of day as seconds from midnight (default 7200 = 02:00).

"The time has the same format as offset except that no leading sign ( '-' or '+' ) is allowed. The default, if time is not given, shall be 02:00:00."
$8.3 https://pubs.opengroup.org/onlinepubs/9699919799/
 -/
Std.Time.TimeZone.TransitionRule.time : Std.Time.TimeZone.TransitionRule → Std.Time.Second.Offset
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.IsPath.below.cons : ∀ {F : PFunctor.{uA, uB}} {motive : (a : PFunctor.Approx.Path F) → (a_1 : F.M) → PFunctor.M.IsPath a a_1 → Prop}
  (xs : PFunctor.Approx.Path F) {a : F.A} (x : F.M) (f : F.B a → F.M) (i : F.B a) (a_1 : x = PFunctor.M.mk ⟨a, f⟩)
  (a_2 : PFunctor.M.IsPath xs (f i)), PFunctor.M.IsPath.below a_2 → motive xs (f i) a_2 → PFunctor.M.IsPath.below ⋯
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.of_mul_symm_eq : ∀ {G : Type u_3} [inst : DivInvMonoid G], ConjAct.ofConjAct.symm = ConjAct.toConjAct
-- Std.Http.Protocol.H1.Config
/-- Connection limits and parser bounds configuration.
 -/
Std.Http.Protocol.H1.Config : Type
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Lax functoriality.  -/
CategoryTheory.Lax.LaxTrans.naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.LaxTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))
      (self.naturality (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).inv
              (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))))))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.lift_ι : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (hs : CategoryTheory.Limits.IsLimit s), CategoryTheory.CategoryStruct.comp (hs.lift t) s.ι = t.ι
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The L-function of the (unique) Dirichlet character mod 1 is the Riemann zeta function.
(Compare `DirichletCharacter.LSeries_modOne_eq`.)
 -/
DirichletCharacter.LFunction_modOne_eq : ∀ {χ : DirichletCharacter ℂ 1}, DirichletCharacter.LFunction χ = riemannZeta