mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Erase
List.eraseP_cons_of_neg : ∀ {α : Type u_1} {a : α} {l : List α} {p : α → Bool}, ¬p a = true → List.eraseP p (a :: l) = a :: List.eraseP p l
-- Mathlib.Data.Int.Fib.Basic
Int.fib.eq_1 : ∀ (n : ℤ),
  Int.fib n = if 0 ≤ n then ↑(Nat.fib n.toNat) else if Even n then -↑(Nat.fib (-n).toNat) else ↑(Nat.fib (-n).toNat)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty_diff_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂
-- Mathlib.Data.Sigma.Order
Sigma.le_def : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LE (α i)] {a b : (i : ι) × α i},
  a ≤ b ↔ ∃ (h : a.fst = b.fst), h ▸ a.snd ≤ b.snd
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.map_biInf_comap : ∀ {α : Type u_1} {ι : Type u_2} {β : Type u_3} {I : Set ι},
  I.Nonempty →
    ∀ {f : α → β} (m : ι → MeasureTheory.OuterMeasure β),
      (MeasureTheory.OuterMeasure.map f) (⨅ i ∈ I, (MeasureTheory.OuterMeasure.comap f) (m i)) =
        ⨅ i ∈ I, (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) (m i))
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_inter_support : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) {s : Set α},
  MeasurableSet s → p.toMeasure (s ∩ p.support) = p.toMeasure s
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.modify_eq_modifyₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (f : β a → β a), m.modify a f = m.modifyₘ a f
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpKind.dsimp : Lean.Elab.Tactic.SimpKind
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.hasLimit_iff_hasTerminal_cone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.HasLimit F ↔ CategoryTheory.Limits.HasTerminal (CategoryTheory.Limits.Cone F)
-- Mathlib.Data.Set.Lattice
Set.compl_sInter : ∀ {α : Type u_1} (S : Set (Set α)), (⋂₀ S)ᶜ = ⋃₀ (compl '' S)
-- ProofWidgets.Component.Panel.Basic
/-- The current term-mode goal, if any.  -/
ProofWidgets.PanelWidgetProps.termGoal? : ProofWidgets.PanelWidgetProps → Option Lean.Widget.InteractiveTermGoal
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
AssociatedPrimes.mem_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  I ∈ associatedPrimes R M ↔ IsAssociatedPrime I M
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.rec_eq : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β)
  (x : F (α ::: MvQPF.Fix F α)), MvQPF.Fix.rec g (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: MvQPF.Fix.rec g) x)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WindowClientCapabilities : Type
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fac' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B : CategoryTheory.ObjectProperty C}
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
  [A.IsVerdierRightLocalizing B] {X Y : C} (s : X ⟶ Y),
  A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ CategoryTheory.CategoryStruct.comp s b = s'
-- Mathlib.RingTheory.Regular.RegularSequence
_private.Mathlib.RingTheory.Regular.RegularSequence.0.RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing.match_3.eq_2 : ∀
  (motive :
    (x : Type u_1) →
      (x_1 : CommRing x) →
        (x_2 : Type u_2) →
          (x_3 : AddCommGroup x_2) →
            (x_4 : Module x x_2) → (x_5 : List x) → RingTheory.Sequence.IsWeaklyRegular x_2 x_5 → Sort u_3)
  (α : Type u_1) (x : CommRing α) (M : Type u_2) (x_1 : AddCommGroup M) (x_2 : Module α M) (r : α) (rs : List α)
  (h : RingTheory.Sequence.IsWeaklyRegular M (r :: rs))
  (h_1 :
    (R : Type u_1) →
      (x : CommRing R) →
        (M : Type u_2) →
          (x_3 : AddCommGroup M) →
            (x_4 : Module R M) → (x_5 : RingTheory.Sequence.IsWeaklyRegular M []) → motive R x M x_3 x_4 [] x_5)
  (h_2 :
    (α : Type u_1) →
      (x : CommRing α) →
        (M : Type u_2) →
          (x_3 : AddCommGroup M) →
            (x_4 : Module α M) →
              (r : α) →
                (rs : List α) →
                  (h : RingTheory.Sequence.IsWeaklyRegular M (r :: rs)) → motive α x M x_3 x_4 (r :: rs) h),
  (match α, x, M, x_1, x_2, r :: rs, h with
    | R, x, M, x_3, x_4, [], x_5 => h_1 R x M x_3 x_4 x_5
    | α, x, M, x_3, x_4, r :: rs, h => h_2 α x M x_3 x_4 r rs h) =
    h_2 α x M x_1 x_2 r rs h
-- Mathlib.RingTheory.Congruence.Basic
/-- Definition of `≤` for congruence relations.  -/
RingCon.le_def : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, c ≤ d ↔ ∀ {x y : R}, c x y → d x y
-- Mathlib.Data.Finite.Defs
/-- **Alias** of the forward direction of `not_infinite_iff_finite`. -/
Finite.of_not_infinite : ∀ {α : Sort u_1}, ¬Infinite α → Finite α
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Embedding of alternating maps into multilinear maps as a linear map.  -/
AlternatingMap.toMultilinearMapLM : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  {S : Type u_10} →
                    [inst_5 : Semiring S] →
                      [inst_6 : Module S N] →
                        [inst_7 : SMulCommClass R S N] → M [⋀^ι]→ₗ[R] N →ₗ[S] MultilinearMap R (fun x => M) N
-- Init.Data.Rat.Lemmas
Rat.le_sub_iff : ∀ {a b c : ℚ}, a ≤ c - b ↔ a + b ≤ c
-- Lean.Server.GoTo
_private.Lean.Server.GoTo.0.Lean.Server.locationLinksFromDecl.declMod? : Lean.Name → Lean.Server.GoToM (Option (Lean.Name × Lean.Lsp.DocumentUri))
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.exists_set_encard_eq_coveringNumber : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.coveringNumber ε A ≠ ⊤ → ∃ C ⊆ A, C.Finite ∧ Metric.IsCover ε A C ∧ C.encard = Metric.coveringNumber ε A
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_apply_self : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x : E), (o.areaForm x) x = 0
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.mk_apply_of_notMem : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {s : Finset ι}
  {f : (i : ↑↑s) → β ↑i} {n : ι}, n ∉ s → ((DirectSum.mk β s) f) n = 0
-- Init.PropLemmas
dite_iff_right_iff : ∀ {p : Prop} [inst : Decidable p] {x : p → Prop} {y : Prop}, ((if h : p then x h else y) ↔ y) ↔ ∀ (h : p), x h ↔ y
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.comap_lieSpan_range_eq : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L)
  {ι : Type u_1} (f : ι → ↥K),
  LieSubalgebra.comap K.incl (LieSubalgebra.lieSpan R L (Set.range (Subtype.val ∘ f))) =
    LieSubalgebra.lieSpan R (↥K) (Set.range f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_inter!_eq_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a m₁ = true → Std.DTreeMap.Internal.Impl.contains a m₂ = true) →
        (m₁.inter! m₂).size = m₁.size
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_smul' : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (X : Ω → ENNReal) {c : ENNReal},
  c ≠ ⊤ → P⁻[c • X | mΩ] =ᵐ[P] c • P⁻[X | mΩ]
-- Mathlib.Data.Finset.Powerset
/-- **Number of Subsets of a Set**  -/
Finset.card_powerset : ∀ {α : Type u_1} (s : Finset α), s.powerset.card = 2 ^ s.card
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.liftFromUnder_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (X_1 : CategoryTheory.Functor J (CategoryTheory.Under X)) (X_2 : CategoryTheory.WithInitial J),
  (CategoryTheory.WithInitial.liftFromUnder.obj X_1).obj X_2 =
    match X_2 with
    | CategoryTheory.WithInitial.of x => (X_1.obj x).right
    | CategoryTheory.WithInitial.star => X
-- Mathlib.Order.Atoms
IsStronglyCoatomic.toIsCoatomic : ∀ (α : Type u_5) [inst : PartialOrder α] [inst_1 : OrderTop α] [IsStronglyCoatomic α], IsCoatomic α
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitIsoColimitCurryCompColim.eq_1 : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)],
  CategoryTheory.Limits.colimitIsoColimitCurryCompColim G =
    Trans.simple (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.Functor.currying.symm.unitIso.app G))
      (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim (CategoryTheory.Functor.curry.obj G))
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
isUniformAddGroup_of_addCommGroup : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  IsUniformAddGroup G
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} (h' : k ∈ t), t.getKey k h' = k
-- Mathlib.Algebra.Algebra.Basic
IsScalarTower.to_smulCommClass : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [IsScalarTower R A M], SMulCommClass R A M
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The underlying magma.  -/
MagmaCat.carrier : MagmaCat → Type u
-- Mathlib.Order.Partition.Finpartition
Equiv.sigmaCongr.eq_1 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ → Type u_3} {β₂ : α₂ → Type u_4} (f : α₁ ≃ α₂)
  (F : (a : α₁) → β₁ a ≃ β₂ (f a)), f.sigmaCongr F = (Equiv.sigmaCongrRight F).trans f.sigmaCongrLeft
-- Mathlib.Order.Hom.Lex
/-- Lexicographic product type with `Unique` type on the right is `OrderIso` to the left.  -/
Prod.Lex.prodUnique : (α : Type u_2) → (β : Type u_3) → [inst : PartialOrder α] → [inst_1 : Preorder β] → [Unique β] → Lex (α × β) ≃o α
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.hasDerivAtFilter_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f₀ f₁ : 𝕜 → F} {f₀' f₁' : F} {L : Filter (𝕜 × 𝕜)},
  Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁ → f₀' = f₁' → (HasDerivAtFilter f₀ f₀' L ↔ HasDerivAtFilter f₁ f₁' L)
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.dest_corec : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β))
  (x : β), (MvQPF.Cofix.corec g x).dest = MvFunctor.map (TypeVec.id ::: MvQPF.Cofix.corec g) (g x)
-- Mathlib.Analysis.Convex.Between
Wbtw.of_le_of_le : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {x y z : R},
  x ≤ y → y ≤ z → Wbtw R x y z
-- Lean.Util.Path
/-- Find the system root of the given `lean` command
by calling `lean --print-prefix` and returning the path it prints.
Defaults to trying the `lean` in `PATH`.
If set, the `LEAN_SYSROOT` environment variable takes precedence.
Note that the called `lean` binary might not be part of the system root,
e.g. in the case of `elan`'s proxy binary.
Users internal to Lean should use `Lean.getBuildDir` instead.
 -/
Lean.findSysroot : optParam String "lean" → IO System.FilePath
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instToJsonRange.toJson : Lean.Lsp.Range → Lean.Json
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.collectDeps.visit : Array Lean.Expr → Lean.Expr → Array ℕ → Array ℕ
-- Mathlib.Topology.Order.LawsonTopology
Topology.lawsonClosed_of_lowerClosed : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α),
  IsClosed (⇑Topology.WithLower.ofLower ⁻¹' s) → IsClosed (⇑Topology.WithLawson.ofLawson ⁻¹' s)
-- Mathlib.Geometry.Convex.Cone.Dual
/-- Duality with respect to a general bilinear map can be expressed as duality using the
standard pairing `Dual.eval`.  -/
PointedCone.dual_eq_comap_dual_eval : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (s : Set M),
  PointedCone.dual p s = PointedCone.comap p.flip (PointedCone.dual (Module.Dual.eval R M) s)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioi_subset_Ioi : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], a ≤ b → Finset.Ioi b ⊆ Finset.Ioi a
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight.eq_1 : ∀ {n : ℕ} (x : BitVec n) (s : ℕ), x.sshiftRight s = BitVec.ofInt n (x.toInt >>> s)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapM.match_1.eq_1 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (Option β')} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) none)
  (h_1 : (hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩)
  (h_2 : (out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩),
  (match ⟨none, hf⟩ with
    | ⟨none, hf⟩ => h_1 hf
    | ⟨some out', hf⟩ => h_2 out' hf) =
    h_1 hf
-- Lean.Util.Trace
Lean.instExceptToTraceResult : {α ε : Type} → Lean.ExceptToTraceResult ε α
-- Init.Data.Vector.Lex
Vector.instAsymmLt : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2], Std.Asymm fun x1 x2 => x1 < x2
-- Mathlib.Analysis.Distribution.Sobolev
/-- The Fourier transform of a Sobolev function of order `s` with `s > d / 2` can be represented by
a `L1` function.

This is the main calculation of the Sobolev embedding theorem.  -/
TemperedDistribution.MemSobolev.fourier_memL1 : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ},
  ↑(Module.finrank ℝ E) < 2 * s →
    ∀ {f : TemperedDistribution E F},
      TemperedDistribution.MemSobolev s 2 f →
        ∃ v, FourierTransform.fourier f = MeasureTheory.Lp.toTemperedDistribution v
-- Mathlib.Data.List.Shortlex
/-- If two lists `s` and `t` have the same length, `s` is smaller than `t` under the shortlex order
over a relation `r`  when `s` is smaller than `t` under the lexicographic order over `r`  -/
List.Shortlex.of_lex : ∀ {α : Type u_1} {r : α → α → Prop} {s t : List α}, s.length = t.length → List.Lex r s t → List.Shortlex r s t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, (m₁.union! m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Init.Tactics
/-- Leaves the stateful proof mode of `Std.Do.SPred`, tries to eta-expand through all definitions
related to the logic of the `Std.Do.SPred` and gently simplifies the resulting pure Lean
proposition. This is often the right thing to do after `mvcgen` in order for automation to prove
the goal.
 -/
Lean.Parser.Tactic.mleaveMacro : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pi.Basic
uniqueOfSurjectiveZero.eq_1 : ∀ (α : Type u_4) {β : Type u_5} [inst : Zero β] (h : Function.Surjective 0),
  uniqueOfSurjectiveZero α h = Function.Surjective.uniqueOfSurjectiveConst α 0 h
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.quotientToQuotientRangePowQuotSuccAux_mk : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S),
  p.quotientToQuotientRangePowQuotSuccAux P a_mem (Submodule.Quotient.mk x) =
    Submodule.Quotient.mk ⟨(Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (a * x), ⋯⟩
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
_private.Mathlib.Geometry.Manifold.VectorField.LieBracket.0.VectorField.mlieBracket.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (V W : (x : M) → TangentSpace I x) (x₀ : M),
  VectorField.mlieBracket I V W x₀ = VectorField.mlieBracketWithin I V W Set.univ x₀
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.toCloseds_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : T2Space α]
  [inst_3 : T2Space β] (K : TopologicalSpace.Compacts α) (L : TopologicalSpace.Compacts β),
  (K ×ˢ L).toCloseds = K.toCloseds ×ˢ L.toCloseds
-- Mathlib.Topology.Closure
closure_eq_interior_union_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s = interior s ∪ frontier s
-- Aesop.Stats.Basic
Aesop.profilingRule : {m : Type → Type} →
  [Monad m] → [Aesop.MonadStats m] → [MonadLiftT BaseIO m] → {α : Type} → Aesop.DisplayRuleName → (α → Bool) → m α → m α
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensRange_pullbackSnd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.pullback.snd f g) =
    (TopologicalSpace.Opens.map g.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the right by a function preserves uniform convergence on a filter  -/
TendstoUniformlyOnFilter.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β}
  {p : Filter ι} {p' : Filter α},
  TendstoUniformlyOnFilter F f p p' →
    ∀ (g : γ → α), TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (Filter.comap g p')
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₁_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  (φ₀ φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ K) (HomologicalComplex.cylinder.desc φ₀ φ₁ h) = φ₁
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftEquiv_id_apply : ∀ {K : Type u_1} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing M] (j : K →+* M) (p : ℕ) [inst_2 : ExpChar M p]
  [inst_3 : ExpChar K p] [inst_4 : PerfectRing M p], (PerfectRing.liftEquiv M (RingHom.id K) p) j = j
-- Init.Data.UInt.Bitwise
UInt64.shiftLeft_xor : ∀ {a b c : UInt64}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Init.Data.Int.Order
Int.neg_pos_of_neg : ∀ {a : ℤ}, a < 0 → 0 < -a
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.tfae : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (f : X → Y),
  [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in nhds x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
-- Batteries.Lean.EStateM
EStateM.run'_throw : ∀ {ε σ α : Type u_1} (e : ε) (s : σ), (throw e).run' s = none
-- Std.Net.Addr
Std.Net.AddressFamily.ipv4 : Std.Net.AddressFamily
-- Lean.Parser.Basic
Lean.Parser.symbolFn : String → Lean.Parser.ParserFn
-- Mathlib.Algebra.BigOperators.Field
Finset.dens_eq_sum_dens_image : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype β] [inst_1 : DecidableEq α] (f : β → α) (t : Finset β),
  t.dens = ∑ a ∈ Finset.image f t, {b ∈ t | f b = a}.dens
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
                        [inst_6 : Q.HasOfPostcompProperty Q] →
                          [inst_7 : Q.IsStableUnderBaseChange] →
                            [inst_8 : Q.IsStableUnderComposition] →
                              (hX : Q (X ↘ S)) →
                                (hW : Q (W ↘ S)) →
                                  (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) →
                                    (j : 𝒰.I₀) →
                                      ((AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).X j).Over S
-- Init.Data.String.Subslice
/-- Constructs a subslice of `s` given the bounds of the subslice and a proof that the subslice
is non-degenerate.
 -/
String.Slice.subslice : (s : String.Slice) → (newStart newEnd : s.Pos) → newStart ≤ newEnd → s.Subslice
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticCode.string.injEq : ∀ (s s_1 : String), (Lean.Lsp.DiagnosticCode.string s = Lean.Lsp.DiagnosticCode.string s_1) = (s = s_1)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.setLhsPrec.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Int.Order.Basic
Int.nonneg_or_nonpos_of_mul_nonneg : ∀ {a b : ℤ}, 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.horiz_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {g : W ⟶ Y} {h : X ⟶ Z} {f : W ≅ X}
  {i : Y ≅ Z}, CategoryTheory.CommSq f.hom g h i.hom → CategoryTheory.CommSq f.inv h g i.inv
-- Lean.Elab.Match
/-- "Discriminant refinement" main loop.
`first?` contains the first error message we found before updated the `discrs`.  -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAltViews.loop : Option Bool →
  Array Lean.Elab.Term.Discr →
    Array Lean.FVarId →
      Lean.Expr →
        Array Lean.Elab.Term.TermMatchAltView →
          Option (Lean.Elab.Term.SavedState × Lean.Exception) →
            Lean.Elab.TermElabM
              (Array Lean.Elab.Term.Discr × Lean.Expr × Array (Lean.Meta.Match.AltLHS × Lean.Expr) × Bool)
-- Init.Notation
/-- When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this
file cannot be read, elaboration fails.
 -/
Lean.includeStr : Lean.ParserDescr
-- Mathlib.NumberTheory.Multiplicity
Nat.eight_dvd_sq_sub_one_of_odd : ∀ {k : ℕ}, Odd k → 8 ∣ k ^ 2 - 1
-- Mathlib.Order.Circular
btw_of_sbtw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b c