mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
mem_primitiveRoots : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R},
  0 < k → (ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k)
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.toIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.WalkingIso C),
  (CategoryTheory.WalkingIso.toIso F).hom = F.map CategoryTheory.WalkingIso.iso.hom
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ},
  f ∈ 𝒜 m → 0 < m → CategoryTheory.IsIso (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousOn_univ : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α),
  EquicontinuousOn F Set.univ ↔ Equicontinuous F
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.descCochain.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cochain F K m),
  α = α_1 →
    ∀ (β β_1 : CochainComplex.HomComplex.Cochain G K n),
      β = β_1 →
        ∀ (h : m + 1 = n) (T : CochainComplex.HomComplex.Triplet n),
          CochainComplex.mappingCone.descCochain φ α β h T = CochainComplex.mappingCone.descCochain φ α_1 β_1 h T
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.closedBall_add : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.addConst_NonnegCoeffs : ∀ {p : Lean.Grind.CommRing.Poly} {k : ℤ}, k ≥ 0 → p.NonnegCoeffs → (p.addConst k).NonnegCoeffs
-- Lean.Structure
Lean.StructureFieldInfo.mk.sizeOf_spec : ∀ (fieldName projFn : Lean.Name) (subobject? : Option Lean.Name) (binderInfo : Lean.BinderInfo)
  (autoParam? : Option Lean.Expr),
  sizeOf
      { fieldName := fieldName, projFn := projFn, subobject? := subobject?, binderInfo := binderInfo,
        autoParam? := autoParam? } =
    1 + sizeOf fieldName + sizeOf projFn + sizeOf subobject? + sizeOf binderInfo + sizeOf autoParam?
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_zero : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K), RatFunc.mk p 0 = { toFractionRing := 0 }
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_inv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
  (x y : G), edist x⁻¹ y = edist x y⁻¹
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciSup_pos : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {p : Prop} {f : p → α} (hp : p), ⨆ (h : p), f h = f hp
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Int.range_nsmulAddMonoidHom : ∀ (n : ℕ), (nsmulAddMonoidHom n).range = AddSubgroup.zmultiples ↑n
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod_comp_snd : ∀ (C : Type u₁) [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] (D : Type u₂)
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] {X Y Z : C × D} (f : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2))
  (g : (Y.1 ⟶ Z.1) × (Y.2 ⟶ Z.2)),
  (CategoryTheory.CategoryStruct.comp f g).2 = CategoryTheory.CategoryStruct.comp f.2 g.2
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.instFinite : ∀ {α : Type w} {m : Type w → Type w'} [inst : Pure m], Std.Iterators.Finite (Std.Iterators.Types.ArrayIterator α) m
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
LinearMap.bound_of_sphere_bound : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ},
  0 < r → ∀ (c : ℝ) (f : E →ₗ[𝕜] 𝕜), (∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ c) → ∀ (z : E), ‖f z‖ ≤ c / r * ‖z‖
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
  (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).getKey k h' = t.getKey k ⋯
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.getSuggestionsCore : Lean.TSyntax `tactic → Array (Lean.TSyntax `tactic)
-- Mathlib.Logic.Equiv.Prod
/-- A variation on `Equiv.prodCongr` where the equivalence in the second component can depend
on the first component. A typical example is a shear mapping, explaining the name of this
declaration.  -/
Equiv.prodShear : {α₁ : Type u_9} → {α₂ : Type u_10} → {β₁ : Type u_11} → {β₂ : Type u_12} → α₁ ≃ α₂ → (α₁ → β₁ ≃ β₂) → α₁ × β₁ ≃ α₂ × β₂
-- Init.Data.UInt.Lemmas
UInt16.le_rfl : ∀ {a : UInt16}, a ≤ a
-- Aesop.Forward.State
/-- Add a hypothesis or pattern substitution to the cluster state.  -/
Aesop.ClusterState.addRawHyp : Aesop.RawHyp → Aesop.Slot → Aesop.ClusterState → Aesop.ClusterState.AddM Aesop.ClusterState
-- Mathlib.Order.Defs.PartialOrder
ne_of_gt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → a ≠ b
-- Mathlib.Algebra.Group.Prod
Prod.instAddMonoid : {M : Type u_3} → {N : Type u_4} → [AddMonoid M] → [AddMonoid N] → AddMonoid (M × N)
-- Mathlib.Data.List.Basic
Function.Involutive.exists_mem_and_apply_eq_iff : ∀ {α : Type u} {f : α → α}, Function.Involutive f → ∀ (x : α) (l : List α), (∃ y ∈ l, f y = x) ↔ f x ∈ l
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_cons : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {b : β}
  (h : b ∉ s), (Finset.cons b s h).sup f = f b ⊔ s.sup f
-- Mathlib.Probability.Independence.Integration
/-- If `X` and `Y` are two independent random variables, `B X Y` is integrable, `Y` is not
almost-surely `0` and `c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ`, then `X` is integrable.

This is useful for the case where `B` is scalar multiplication, as it will allow to drop
integrability hypotheses.  -/
ProbabilityTheory.IndepFun.integrable_left_of_integrable_op : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E]
  [inst_4 : NormedAddGroup F] [inst_5 : MeasurableSpace F] [OpensMeasurableSpace F] [inst_7 : TopologicalSpace G]
  [inst_8 : ContinuousENorm G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    ∀ (B : E → F → G) (c : NNReal),
      c ≠ 0 →
        (∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ) →
          MeasureTheory.Integrable (fun ω => B (X ω) (Y ω)) μ →
            MeasureTheory.AEStronglyMeasurable X μ →
              MeasureTheory.AEStronglyMeasurable Y μ → ¬Y =ᵐ[μ] 0 → MeasureTheory.Integrable X μ
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.toQ_add : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a b : α),
  Lean.Grind.IntModule.OfNatModule.toQ (a + b) =
    Lean.Grind.IntModule.OfNatModule.toQ a + Lean.Grind.IntModule.OfNatModule.toQ b
-- Mathlib.Algebra.Group.WithOne.Defs
/-- The canonical map from `α` into `WithOne α`  -/
WithOne.coe : {α : Type u} → α → WithOne α
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix_of_basis_mulVec : ∀ {ι : Type w} {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Fintype ι] (b : Module.Basis ι A B) (z : B),
  (Algebra.traceMatrix A ⇑b).mulVec (b.equivFun z) = fun i => (Algebra.trace A B) (z * b i)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The bicategory of comonads in `B`.  -/
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.inst : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → CategoryTheory.Bicategory (CategoryTheory.Bicategory.OplaxTrans.ComonadBicat B)
-- Mathlib.CategoryTheory.Monoidal.Linear
CategoryTheory.tensorRight_linear : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.MonoidalCategory C] [inst_5 : CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.MonoidalLinear R C] (X : C),
  CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.tensorRight X)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.zero : Nat.Partrec.Code
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget GrpCat)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.field.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.field = 1
-- Lean.Meta.Check
/-- Given two expressions `a` and `b`, this method tries to annotate terms with `pp.explicit := true`
and other `pp` options to expose "implicit" differences.
For example, suppose `a` and `b` are of the form
```lean
@HashMap Nat Nat eqInst hasInst1
@HashMap Nat Nat eqInst hasInst2
```
By default, the pretty printer formats both of them as `HashMap Nat Nat`.
So, counterintuitive error messages such as
```lean
error: application type mismatch
  HashMap.insert m
argument
  m
has type
  HashMap Nat Nat
but is expected to have type
  HashMap Nat Nat
```
would be produced.
By adding `pp.explicit := true`, we can generate the more informative error
```lean
error: application type mismatch
  HashMap.insert m
argument
  m
has type
  @HashMap Nat Nat eqInst hasInst1
but is expected to have type
  @HashMap Nat Nat eqInst hasInst2
```

Remark: this method implements simple heuristics; we should extend it as we find other counterintuitive
error messages.
 -/
Lean.Meta.addPPExplicitToExposeDiff : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Lie.Basic
/-- A morphism of Lie algebras is compatible with brackets.  -/
LieHom.map_lie' : ∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (self : L →ₗ⁅R⁆ L') {x y : L},
  (↑self).toFun ⁅x, y⁆ = ⁅(↑self).toFun x, (↑self).toFun y⁆
-- Lean.Class
/-- Position of the class `outParams`.
For example, for class
```
class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
```
`outParams := #[2, 3]`
 -/
Lean.ClassEntry.outParams : Lean.ClassEntry → Array ℕ
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.add' : ∀ {A : Type u} {inst : AddGroup A} [self : AddGroupFilterBasis A] {U : Set A},
  U ∈ self.sets → ∃ V ∈ self.sets, V + V ⊆ U
-- Init.Data.Range.Polymorphic.NatLemmas
Std.PRange.Nat.succMany?_eq : ∀ {m n : ℕ}, Std.PRange.succMany? n m = some (m + n)
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.isPrincipal_inv : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) [(↑I).IsPrincipal],
  I ≠ 0 → (↑I⁻¹).IsPrincipal
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- The discrete subcategory of objects in normal form includes into the free monoidal category.  -/
CategoryTheory.FreeMonoidalCategory.inclusion : {C : Type u} →
  CategoryTheory.Functor ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
    (CategoryTheory.FreeMonoidalCategory C)
-- Mathlib.Algebra.Ring.Identities
/-- Brahmagupta-Fibonacci identity or Diophantus identity, see
<https://en.wikipedia.org/wiki/Brahmagupta%E2%80%93Fibonacci_identity>.

This sign choice here corresponds to the signs obtained by multiplying two complex numbers.
 -/
sq_add_sq_mul_sq_add_sq : ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ y₁ y₂ : R},
  (x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.spec_punit_isEmpty : IsEmpty ↥(AlgebraicGeometry.Spec (CommRingCat.of PUnit.{u + 1}))
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sSameSide_excenter_singleton_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  {i j : Fin (n + 1)},
  i ≠ j → (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.excenter {j}) (s.points i)
-- Std.Time.Format.Modifier
/-- `N`: Nanosecond of day (e.g., 1234000000).
 -/
Std.Time.Modifier.N : Std.Time.Number → Std.Time.Modifier
-- Init.Data.SInt.Lemmas
Int64.add_sub_cancel : ∀ (a b : Int64), a + b - b = a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_get?_eq_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a : α},
  (t.get? a).isSome = t.contains a
-- Mathlib.Data.ENNReal.Basic
ENNReal.lt_iff_exists_rat_btwn : ∀ {a b : ENNReal}, a < b ↔ ∃ q, 0 ≤ q ∧ a < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
-- Init.Data.UInt.Bitwise
USize.ne_not_self : ∀ {a : USize}, a ≠ ~~~a
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- `g ∘ f` is `C^n` within `s` at `x` if `g` is `C^n` at `f x` and
`f` is `C^n` within `s` at `x`.  -/
ContMDiffAt.comp_contMDiffWithinAt_of_eq : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {g : M' → M''} {x : M} {y : M'},
  ContMDiffAt I' I'' n g y → ContMDiffWithinAt I I' n f s x → f x = y → ContMDiffWithinAt I I'' n (g ∘ f) s x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.StrongEpiMonoFactorisation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
  {toMonoFactorisation : CategoryTheory.Limits.MonoFactorisation f}
  {e_strong_epi : CategoryTheory.StrongEpi toMonoFactorisation.e}
  {toMonoFactorisation_1 : CategoryTheory.Limits.MonoFactorisation f}
  {e_strong_epi_1 : CategoryTheory.StrongEpi toMonoFactorisation_1.e},
  { toMonoFactorisation := toMonoFactorisation, e_strong_epi := e_strong_epi } =
      { toMonoFactorisation := toMonoFactorisation_1, e_strong_epi := e_strong_epi_1 } →
    toMonoFactorisation = toMonoFactorisation_1
-- Init.Data.String.Iterate
String.Slice.RevPosIterator.mk.sizeOf_spec : ∀ {s : String.Slice} (currPos : s.Pos), sizeOf { currPos := currPos } = 1 + sizeOf currPos
-- Mathlib.Analysis.Fourier.AddCircle
fourier_neg : ∀ {T : ℝ} {n : ℤ} {x : AddCircle T}, (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv.inj : ∀ {e : Lean.Expr} {f g : Mathlib.Tactic.BicategoryLike.Mor₁} {η : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {e_1 : Lean.Expr} {f_1 g_1 : Mathlib.Tactic.BicategoryLike.Mor₁} {η_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso},
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e f g η = Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e_1 f_1 g_1 η_1 →
    e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ η = η_1
-- Mathlib.Data.List.Cycle
Cycle.mk''_eq_coe : ∀ {α : Type u_1} (l : List α), Quotient.mk'' l = ↑l
-- Mathlib.Topology.LocallyFinite
/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
function `F : Π a, β a` such that for any `x`, for sufficiently large values of `n`, we have
`f n y = F y` in a neighbourhood of `x`.  -/
LocallyFinite.exists_forall_eventually_atTop_eventually_eq' : ∀ {X : Type u_4} [inst : TopologicalSpace X] {π : X → Sort u_6} {f : ℕ → (x : X) → π x},
  (LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) →
    ∃ F, ∀ (x : X), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ᶠ (y : X) in nhds x, f n y = F y
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_map_eq`. -/
Ideal.ramificationIdx_map_eq : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {S₁ : Type u_1} [inst_3 : CommRing S₁] [inst_4 : Algebra R S₁] {E : Type u_2} [inst_5 : EquivLike E S S₁]
  [AlgEquivClass E R S S₁] (P : Ideal S) (e : E), p.ramificationIdx' (Ideal.map e P) = p.ramificationIdx' P
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  M.equivMonComonUnitIsoAppX.inv.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.liftCycles.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k k_1 : A ⟶ K.X i) (e_k : k = k_1) (j j_1 : ι) (e_j : j = j_1) (hj : c.next i = j)
  (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0), K.liftCycles k j hj hk = K.liftCycles k_1 j_1 ⋯ ⋯
-- Lean.Server.Requests
Lean.Server.RequestHandlerCompleteness.complete : Lean.Server.RequestHandlerCompleteness
-- Init.Data.SInt.Basic
Int16.ofUInt16.inj : ∀ {toUInt16 toUInt16_1 : UInt16}, { toUInt16 := toUInt16 } = { toUInt16 := toUInt16_1 } → toUInt16 = toUInt16_1
-- Mathlib.NumberTheory.GaussSum
_private.Mathlib.NumberTheory.GaussSum.0.gaussSum_mul_aux : ∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'}, χ ≠ 1 → ∀ (ψ : AddChar R R') (b : R), ∑ a, χ (a * b⁻¹) * ψ (a - b) = ∑ c, χ c * ψ (b * (c - 1))
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
Std.Iter.step_takeWhile : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} {it : Std.Iter β},
  (Std.Iter.takeWhile P it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ =>
      match hP : P out with
      | true => Std.PlausibleIterStep.yield (Std.Iter.takeWhile P it') out ⋯
      | false => Std.PlausibleIterStep.done ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.takeWhile P it') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
-- Mathlib.RingTheory.PowerSeries.WellKnown
/-- The theorem `PowerSeries.mk_one_mul_one_sub_eq_one` implies that `1 - X` is a unit in `S⟦X⟧`
whose inverse is the power series `1 + X + X^2 + ...`. This theorem states that for any `d : ℕ`,
`PowerSeries.invOneSubPow S d` is equal to `(1 - X)⁻¹ ^ d`.
 -/
PowerSeries.invOneSubPow_eq_inv_one_sub_pow : ∀ (S : Type u_1) [inst : CommRing S] (d : ℕ),
  PowerSeries.invOneSubPow S d = (Units.mkOfMulEqOne (1 - PowerSeries.X) (PowerSeries.mk 1) ⋯)⁻¹ ^ d
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_zero : Nat.factorial 0 = 1
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.lt_pow_go_succ : ∀ {n a guess fuel : ℕ}, a < (guess + 1) ^ (n + 2) → a < (Nat.nthRoot.go n a fuel guess + 1) ^ (n + 2)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.MutualMeasure.func.sizeOf_spec : ∀ (a : ℕ), sizeOf (Lean.Elab.WF.GuessLex.MutualMeasure.func a) = 1 + sizeOf a
-- Lean.Compiler.LCNF.Types
/-- tagged` is a tagged pointer (i.e., the least significant bit is 1) storing a scalar value.
 -/
Lean.Compiler.LCNF.ImpureType.tagged : Lean.Expr
-- Aesop.Tree.Data
Aesop.GoalState.provenByRuleApplication : Aesop.GoalState
-- Mathlib.Data.List.Chain
/-- Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
the predicate is true everywhere in the chain and at `a`.
That is, we can propagate the predicate up the chain.
 -/
List.IsChain.backwards_concat_induction : ∀ {α : Type u_1} {r : α → α → Prop} {b : α} (p : α → Prop) (l : List α),
  List.IsChain r (l ++ [b]) → (∀ ⦃x y : α⦄, r x y → p y → p x) → p b → ∀ i ∈ l, p i
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
Filter.EventuallyEq.mdifferentiableAt_iff : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M},
  f₁ =ᶠ[nhds x] f → (MDiffAt f₁ x ↔ MDiffAt f x)
-- Mathlib.GroupTheory.Commensurable
AddSubgroup.Commensurable.symm : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.Commensurable K → K.Commensurable H
-- Init.Data.SInt.Lemmas
ISize.ofIntTruncate_int8ToInt : ∀ (x : Int8), ISize.ofIntClamp x.toInt = x.toISize
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.instInfSetColexForall : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] → [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedGT ι] → InfSet (Colex ((i : ι) → α i))
-- Mathlib.Tactic.Translate.Core
/-- `(attr := ...)` applies the given attributes to the original and the translated declaration.
In the case of `to_additive`, we may want to apply it multiple times,
(such as in `a ^ n` -> `n • a` -> `n +ᵥ a`). In this case, you should use the syntax
`to_additive (attr := some_other_attr, to_additive)`, which will apply `some_other_attr` to all
three generated declarations.
 -/
Mathlib.Tactic.Translate.attrOption : Lean.ParserDescr
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_above_le`. -/
Ideal.ramificationIdx'_above_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T], r.ramificationIdx S ≤ r.ramificationIdx R
-- Init.Data.Range.Polymorphic.PRange
Std.Roo.LawfulRcoIntersection.mk : ∀ {α : Type w} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.Roo.HasRcoIntersection α],
  (∀ {a : α} {r : Std.Roo α} {s : Std.Rco α}, a ∈ Std.Roo.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s) →
    Std.Roo.LawfulRcoIntersection α
-- Mathlib.Topology.Algebra.MulAction
AddAction.continuousVAdd_compHom : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : AddMonoid M]
  [inst_3 : AddAction M X] [ContinuousVAdd M X] {N : Type u_5} [inst_5 : TopologicalSpace N] [inst_6 : AddMonoid N]
  {f : N →+ M}, Continuous ⇑f → ContinuousVAdd N X
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects colimits, then `F : Cᵒᵖ ⥤ D` reflects limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F