mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.Machine.mk.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {reader : Std.Http.Protocol.H1.Reader dir}
  {writer : Std.Http.Protocol.H1.Writer dir} {config : Std.Http.Protocol.H1.Config}
  {events : Array (Std.Http.Protocol.H1.Event dir)} {error : Option Std.Http.Protocol.H1.Error}
  {instant : Option Std.Time.PlainDateTime} {keepAlive forcedFlush pullBodyStalled : Bool}
  {reader_1 : Std.Http.Protocol.H1.Reader dir} {writer_1 : Std.Http.Protocol.H1.Writer dir}
  {config_1 : Std.Http.Protocol.H1.Config} {events_1 : Array (Std.Http.Protocol.H1.Event dir)}
  {error_1 : Option Std.Http.Protocol.H1.Error} {instant_1 : Option Std.Time.PlainDateTime}
  {keepAlive_1 forcedFlush_1 pullBodyStalled_1 : Bool},
  { reader := reader, writer := writer, config := config, events := events, error := error, instant := instant,
        keepAlive := keepAlive, forcedFlush := forcedFlush, pullBodyStalled := pullBodyStalled } =
      { reader := reader_1, writer := writer_1, config := config_1, events := events_1, error := error_1,
        instant := instant_1, keepAlive := keepAlive_1, forcedFlush := forcedFlush_1,
        pullBodyStalled := pullBodyStalled_1 } →
    reader = reader_1 ∧
      writer = writer_1 ∧
        config = config_1 ∧
          events = events_1 ∧
            error = error_1 ∧
              instant = instant_1 ∧
                keepAlive = keepAlive_1 ∧ forcedFlush = forcedFlush_1 ∧ pullBodyStalled = pullBodyStalled_1
-- Mathlib.Topology.Continuous
ContinuousAt.congr : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X}
  {g : X → Y}, ContinuousAt f x → f =ᶠ[nhds x] g → ContinuousAt g x
-- Mathlib.RingTheory.AdicCompletion.Basic
Hausdorffification.induction_on : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {C : Hausdorffification I M → Prop} (x : Hausdorffification I M), (∀ (x : M), C ((Hausdorffification.of I M) x)) → C x
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.nsmul_vadd_mod_minimalPeriod : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] (a : G) (b : α) (n : ℕ),
  (n % Function.minimalPeriod (fun x => a +ᵥ x) b) • a +ᵥ b = n • a +ᵥ b
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map₂_coe_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : WithOne β),
  WithOne.map₂ f (↑a) b = WithOne.map (fun b => f a b) b
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.congr_fun : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] {f g : A →ₛₙₐ[φ] B}, f = g → ∀ (x : A), f x = g x
-- Mathlib.CategoryTheory.Opposites
/-- Given a natural transformation `α : F.leftOp ⟶ G.leftOp`, for `F G : C ⥤ Dᵒᵖ`,
taking `op` of each component gives a natural transformation `G ⟶ F`.
 -/
CategoryTheory.NatTrans.removeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C Dᵒᵖ} → (F.leftOp ⟶ G.leftOp) → (G ⟶ F)
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.mk.injEq : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (toFun : α → β)
  (edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun x) (toFun y) = ↑r * edist x y) (toFun_1 : α → β)
  (edist_eq'_1 : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun_1 x) (toFun_1 y) = ↑r * edist x y),
  ({ toFun := toFun, edist_eq' := edist_eq' } = { toFun := toFun_1, edist_eq' := edist_eq'_1 }) = (toFun = toFun_1)
-- Init.Data.Array.Monadic
Array.findSomeM?_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → Option β}
  {xs : Array α}, Array.findSomeM? (fun x => pure (f x)) xs = pure (Array.findSome? f xs)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.cg_closure : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {s : Set M},
  s.Countable → ((FirstOrder.Language.Substructure.closure L).toFun s).CG
-- Mathlib.Order.Filter.Defs
/-- The principal filter of `s` is the collection of all supersets of `s`.  -/
Filter.principal : {α : Type u_1} → Set α → Filter α
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν ν' : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν']
  [MeasureTheory.SigmaFinite ν'], μ.MutuallySingular ν → ν.AbsolutelyContinuous ν' → μ.rnDeriv ν' =ᵐ[ν] 0
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_le_im_iff_eq_I_mul_norm : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, ‖z‖ ≤ RCLike.im z ↔ z = RCLike.I * ↑‖z‖
-- Mathlib.Order.Lattice
sup_rotate' : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ (b ⊔ c) = b ⊔ (c ⊔ a)
-- Lean.Expr
/-- `(fun x => e) a` ==> `e[x/a]`.  -/
Lean.Expr.headBeta : Lean.Expr → Lean.Expr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).isEmpty = ((t.erase k).isEmpty && (f t[k]?).isNone)
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.codChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x), h.codChart ∈ IsManifold.maximalAtlas J n N
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeMap.Raw.unitOfList l cmp).getKey! k' = k
-- Lean.Meta.Tactic.Replace
/-- Executes the revert/intro pattern, running the continuation `k` after temporarily reverting
the given local variables from the local context of the metavariable `mvarId`,
and then re-introducing the local variables specified by `k`.

- `mvarId` is the goal metavariable to operate on.
- `fvarIds` is an array of `fvarIds` to revert in the order specified.
  An error is thrown if they cannot be reverted in order.
- `clearAuxDeclsInsteadOfRevert` is configuration passed to `Lean.MVarId.revert`.
- `k` is the continuation run once the local variables have been reverted.
  It is provided `mvarId` after the requested variables have been reverted along with the array of reverted variables.
  This array always contains `fvarIds`, but it may contain additional variables that were reverted due to dependencies.
  The continuation returns a value, a new goal, and an _aliasing array_.

Once `k` has completed, one variable is introduced per entry in the aliasing array.
* If the entry is `none`, the variable is just introduced.
* If the entry is `some fv` (where `fv` is a variable from `fvarIds`),
  the variable is introduced and then recorded as an alias of `fv` in the info tree.
  This for example causes the unused variable linter as seeing `fv` and this newly introduced variable as being "the same".

For example, if `k` leaves all the reverted variables in the same order,
having it return `fvars.map .some` as the aliasing array causes those variables to be re-introduced and aliased
to the original local variables.

Returns the value returned by `k` along with the resulting goal after variable introduction.

See `Lean.MVarId.changeLocalDecl` for an example. The motivation is that to work on a local variable,
you need to move it into the goal, alter the goal, and then bring it back into the local context,
all while keeping track of any other local variables that depend on this one.
 -/
Lean.MVarId.withReverted : {α : Type} →
  Lean.MVarId →
    Array Lean.FVarId →
      (Lean.MVarId → Array Lean.FVarId → Lean.MetaM (α × Array (Option Lean.FVarId) × Lean.MVarId)) →
        optParam Bool false → Lean.MetaM (α × Lean.MVarId)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.isLocalHom_stalkMap_congr : ∀ {X Y : AlgebraicGeometry.RingedSpace} (f g : X ⟶ Y),
  f = g →
    ∀ (x : ↑↑X.toPresheafedSpace),
      IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x)) →
        IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap g.hom x))
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerRight_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {Fₗ Gₗ : CategoryTheory.Functor C E} (α : Fₗ ≅ Gₗ)
  (H : CategoryTheory.Functor D E'),
  (CategoryTheory.Join.mapIsoWhiskerRight α H).inv = CategoryTheory.Join.mapWhiskerRight α.inv H
-- Init.Data.Vector.Lemmas
Vector.getElem?_toList : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, xs.toList[i]? = xs[i]?
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_sup : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : Algebra R B]
  [inst_8 : StarRing B] [inst_9 : StarModule R B] (f : A →⋆ₐ[R] B) (S T : StarSubalgebra R A),
  StarSubalgebra.map f (S ⊔ T) = StarSubalgebra.map f S ⊔ StarSubalgebra.map f T
-- Mathlib.Combinatorics.Additive.Dissociation
/-- **Alias** of the reverse direction of `addDissociated_neg`. -/
AddDissociated.neg : ∀ {α : Type u_1} [inst : AddCommGroup α] {s : Set α}, AddDissociated s → AddDissociated (-s)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.move.sizeOf_spec : ∀ {Γ : Type u_1} [inst : SizeOf Γ] (a : Turing.Dir), sizeOf (Turing.TM0.Stmt.move a) = 1 + sizeOf a
-- Lean.Elab.Level
Lean.Elab.Level.State.mctx : Lean.Elab.Level.State → Lean.MetavarContext
-- Mathlib.Data.Complex.Basic
Complex.re_sq_le_normSq : ∀ (z : ℂ), z.re * z.re ≤ Complex.normSq z
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_one : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F},
  Set.InjOn v ↑s → s.Nonempty → (Lagrange.interpolate s v) 1 = 1
-- Mathlib.Data.Seq.Computation
Computation.Equiv.refl : ∀ {α : Type u} (s : Computation α), s.Equiv s
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.int_mul_eq_of_eq_zero : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocRing α] [inst_1 : SubtractionMonoid β],
  Function.Antiperiodic f c → f 0 = 0 → ∀ (n : ℤ), f (↑n * c) = 0
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- Proper group action in the sense of Bourbaki:
the map `G × X → X × X` is a proper map (see `IsProperMap`).  -/
ProperVAdd.isProperMap_vadd_pair : ∀ {G : Type u_1} {X : Type u_2} {inst : TopologicalSpace G} {inst_1 : TopologicalSpace X} {inst_2 : AddGroup G}
  {inst_3 : AddAction G X} [self : ProperVAdd G X], IsProperMap fun gx => (gx.1 +ᵥ gx.2, gx.2)
-- ProofWidgets.Util
instMonadSaveCtxStateT : {m n : Type → Type} → [Monad m] → [MonadSaveCtx m n] → {σ : Type} → MonadSaveCtx (StateT σ m) n
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.span_singleton_dvd_span_singleton_iff_dvd : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R},
  Ideal.span {a} ∣ Ideal.span {b} ↔ a ∣ b
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.evalAlt : Lean.MVarId → Lean.Syntax → Lean.Elab.TermElabM Unit → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A homomorphism from a uniform group to a discrete uniform group is continuous if and only if
its kernel is open.  -/
IsUniformGroup.uniformContinuous_iff_isOpen_ker : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {hom : Type u_3}
  [inst_3 : UniformSpace β] [DiscreteTopology β] [inst_5 : Group β] [IsUniformGroup β] [inst_7 : FunLike hom α β]
  [inst_8 : MonoidHomClass hom α β] {f : hom}, UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
-- Mathlib.RingTheory.Kaehler.Basic
/-- `Ω[S⁄R]` is trivial if `R → S` is surjective.
Also see `Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential`.  -/
KaehlerDifferential.subsingleton_of_surjective : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Function.Surjective ⇑(algebraMap R S) → Subsingleton Ω[S⁄R]
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.le_mul_of_le_mul_inv : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, c < 0 → a ≤ b * c⁻¹ → b ≤ a * c
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, m.keys.contains k = m.contains k
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode.fixed : ℕ → Std.Http.Protocol.H1.Machine.BodyMode✝
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_span_singleton_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Module.IsTorsionBySet R M ↑(R ∙ a) ↔ Module.IsTorsionBy R M a
-- Batteries.Recycling.RBTree.Basic
/-- Concatenate two trees with the same black-height.  -/
RBTree.RBNode.append : {α : Type u_1} → RBTree.RBNode α → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp),
  CategoryTheory.Limits.coneRightOpOfCoconeEquiv.inverse.obj c =
    Opposite.op (CategoryTheory.Limits.coconeOfConeRightOp c)
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- The tangent cone at a non-isolated point contains `0`.  -/
zero_mem_tangentConeAt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E}, x ∈ closure s → 0 ∈ tangentConeAt 𝕜 s x
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
/-- A graph is strongly regular with parameters `n k ℓ μ` if
* its vertex set has cardinality `n`
* it is regular with degree `k`
* every pair of adjacent vertices has `ℓ` common neighbors
* every pair of nonadjacent vertices has `μ` common neighbors
 -/
SimpleGraph.IsSRGWith : {V : Type u} → [Fintype V] → (G : SimpleGraph V) → [DecidableRel G.Adj] → ℕ → ℕ → ℕ → ℕ → Prop
-- Aesop.Tree.Traversal
Aesop.TreeRef.rapp : Aesop.RappRef → Aesop.TreeRef
-- Init.Data.Vector.Lemmas
Vector.toList.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), xs.toList = xs.toArray.toList
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presieve.isSheafFor_of_factorsThru : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] {X : C} {S T : CategoryTheory.Presieve X}
  (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
  S.FactorsThru T →
    CategoryTheory.Presieve.IsSheafFor P S →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, CategoryTheory.Presieve.IsSeparatedFor P R ∧ R.FactorsThruAlong S f) →
        CategoryTheory.Presieve.IsSheafFor P T
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_le_iff_le_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K : Subgroup G} {H : Subgroup N},
  Subgroup.map f K ≤ H ↔ K ≤ Subgroup.comap f H
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct : {C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D
-- Init.Core
Std.instCommutativeOr : Std.Commutative Or
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.norm_eq_zero : ∀ {x : GaussianInt}, Zsqrtd.norm x = 0 ↔ x = 0
-- Mathlib.LinearAlgebra.RootSystem.Chain
/-- If `α = P.root i` and `β = P.root j` are linearly independent, this is the value `p ≥ 0` where
`β - q • α, ..., β - α, β, β + α, ..., β + p • α` is the `α`-chain through `β`.

In the absence of linear independence, it takes a junk value.  -/
RootPairing.chainTopCoeff : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [Finite ι] →
          [inst : CommRing R] →
            [CharZero R] →
              [IsDomain R] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : AddCommGroup N] →
                      [inst_6 : Module R N] → {P : RootPairing ι R M N} → [P.IsCrystallographic] → ι → ι → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.homologyMap'_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  CategoryTheory.ShortComplex.homologyMap' (-φ) h₁ h₂ = -CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂
-- Mathlib.Analysis.RCLike.Basic
/-- Conjugate as an `ℝ`-algebra equivalence  -/
RCLike.conjAe : {K : Type u_1} → [inst : RCLike K] → Gal(K/ℝ)
-- Mathlib.Algebra.Regular.SMul
IsSMulRegular.eq_1 : ∀ {R : Type u_1} (M : Type u_3) [inst : SMul R M] (c : R), IsSMulRegular M c = Function.Injective fun x => c • x
-- Init.Data.Ord.Basic
Ordering.swap_eq_gt : ∀ {o : Ordering}, o.swap = Ordering.gt ↔ o = Ordering.lt
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_neg : ∀ {G : Type u_1} [inst : AddGroup G] (x : G), addOrderOf (-x) = addOrderOf x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- A cochain of degree `0` from `F` to `G` can be constructed from a family
of morphisms `F.X p ⟶ G.X p` for all `p : ℤ`.  -/
CochainComplex.HomComplex.Cochain.ofHoms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} → ((p : ℤ) → F.X p ⟶ G.X p) → CochainComplex.HomComplex.Cochain F G 0
-- Init.Data.Ord.Basic
compareLex_eq_eq : ∀ {α : Sort u_1} {cmp₁ cmp₂ : α → α → Ordering} {a b : α},
  compareLex cmp₁ cmp₂ a b = Ordering.eq ↔ cmp₁ a b = Ordering.eq ∧ cmp₂ a b = Ordering.eq
-- Std.Tactic.BVDecide.Syntax
/-- Don't set additional SAT solver flags.
 -/
Lean.Elab.Tactic.BVDecide.SolverMode.default : Lean.Elab.Tactic.BVDecide.SolverMode
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of an inner regular measure under right multiplication is again inner regular.  -/
MeasureTheory.innerRegular_map_mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.InnerRegular] (g : G),
  (MeasureTheory.Measure.map (fun x => x * g) μ).InnerRegular
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_filter : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad n Pred EPred] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Std.IterM m β}
  {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄ Std.IterM.foldM (fun d b => if f b = true then g d b else pure d) init it ⦃ Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.filter f it) ⦃ Q; eQ ⦄
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean, weighted
version for `NNReal`-valued functions.  -/
NNReal.geom_mean_le_arith_mean_weighted : ∀ {ι : Type u} (s : Finset ι) (w z : ι → NNReal), ∑ i ∈ s, w i = 1 → ∏ i ∈ s, z i ^ ↑(w i) ≤ ∑ i ∈ s, w i * z i
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.hom_ext : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} {f g : A ⟶ B},
  CommBialgCat.Hom.hom f = CommBialgCat.Hom.hom g → f = g
-- Init.Notation
Lean.guardMsgsWhitespaceArg : Lean.ParserDescr
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.le_comap_addConGen : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (r : N → N → Prop) (f : M → N)
  (hf : ∀ (x y : M), f (x + y) = f x + f y), addConGen (Function.onFun r f) ≤ AddCon.comap f hf (addConGen r)
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodFunctorToFunctorProdAssociator_hom_app_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A]
  (X : (CategoryTheory.Functor A C × CategoryTheory.Functor A D) × CategoryTheory.Functor A E) (X_1 : A),
  ((CategoryTheory.prod.prodFunctorToFunctorProdAssociator C D E A).hom.app X).app X_1 =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.1.1.obj X_1))
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.1.2.obj X_1))
        (CategoryTheory.CategoryStruct.id (X.2.obj X_1)))
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofan_inj_f_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C}
  (i : 𝒜) (x : (f i).I), (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f x).fst = i
-- Init.Data.Array.Lemmas
Array.push_beq_push : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {xs ys : Array α}, (xs.push a == ys.push b) = (xs == ys && a == b)
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instSDiffOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → SDiff (Std.ExtDHashMap α β)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_mk' : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (c : RingCon R), ⇑c.mk' = RingCon.toQuotient
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.instHomFunctorRightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal], CategoryTheory.NatTrans.IsMonoidal F.rightUnitor.hom
-- Init.Data.SInt.Lemmas
ISize.toBitVec_minValue : ISize.minValue.toBitVec = BitVec.intMin System.Platform.numBits