mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Queries
/-- Applies the given function to the mappings in the tree in ascending order.  -/
Std.DTreeMap.Internal.Impl.forM : {α : Type u} →
  {β : α → Type v} →
    {m : Type u_1 → Type u_2} →
      [Monad m] → ((a : α) → β a → m PUnit.{u_1 + 1}) → Std.DTreeMap.Internal.Impl α β → m PUnit.{u_1 + 1}
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (n d : aig.RefVec w)
  (wn wr : ℕ) (q r : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r =
    match curr with
    | 0 => { aig := aig, q := q, r := r, hle := ⋯ }
    | curr.succ =>
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r;
      let aig_1 := res.aig;
      let wn_1 := res.wn;
      let wr_1 := res.wr;
      let q_1 := res.q;
      let r_1 := res.r;
      have this := ⋯;
      let n_1 := n.cast this;
      let d_1 := d.cast this;
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig_1 curr n_1 d_1 wn_1 wr_1 q_1 r_1;
      let aig_2 := res.aig;
      have q_2 := res.q;
      have r_2 := res.r;
      have this := ⋯;
      { aig := aig_2, q := q_2, r := r_2, hle := this }
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.getAppUpToDefeq.go : Array Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.Expr)
-- Mathlib.Tactic.ITauto
/-- A variant on `Proof.app'` that performs opportunistic simplification.
(This doesn't do full normalization because we don't want the proof size to blow up.)  -/
Mathlib.Tactic.ITauto.Proof.app : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_eq_none_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.maxKey? = none ↔ t.isEmpty = true)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
BirdDet.Spec.stepEntry_eq : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A F : Matrix (Fin n) (Fin n) R),
  BirdDet.Spec.stepEntry A F = Matrix.of fun i j => (-∑ k > i, F k k) * A i j + ∑ k > i, F i k * A k j
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.of.injEq : ∀ (α : Type u) [isCommRing : CommRing α] [isTopologicalSpace : TopologicalSpace α]
  [isTopologicalRing : IsTopologicalRing α] (α_1 : Type u) (isCommRing_1 : CommRing α_1)
  (isTopologicalSpace_1 : TopologicalSpace α_1) (isTopologicalRing_1 : IsTopologicalRing α_1),
  (TopCommRingCat.of α = TopCommRingCat.of α_1) =
    (α = α_1 ∧ isCommRing ≍ isCommRing_1 ∧ isTopologicalSpace ≍ isTopologicalSpace_1)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- In a complete space, a function which is analytic at a point is also `C^ω` there.
Note that the same statement for `AnalyticOn` does not require completeness, see
`AnalyticOn.contDiffOn`.  -/
AnalyticAt.contDiffAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : WithTop ℕ∞} [CompleteSpace F], AnalyticAt 𝕜 f x → ContDiffAt 𝕜 n f x
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- The sign for each index  -/
ComplexShape.EulerCharSigns.χ : {ι : Type u_1} → (c : ComplexShape ι) → [self : c.EulerCharSigns] → ι → ℤˣ
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.fold.match_1.eq_1 : ∀ {α : Type u_2} (motive : (x : ℕ) → ((i : ℕ) → i < x → α → α) → α → Sort u_1) (f : (i : ℕ) → i < 0 → α → α) (a : α)
  (h_1 : (f : (i : ℕ) → i < 0 → α → α) → (a : α) → motive 0 f a)
  (h_2 : (n : ℕ) → (f : (i : ℕ) → i < n.succ → α → α) → (a : α) → motive n.succ f a),
  (match 0, f, a with
    | 0, f, a => h_1 f a
    | n.succ, f, a => h_2 n f a) =
    h_1 f a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokensLegend : Lean.ToJson Lean.Lsp.SemanticTokensLegend
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.Std.Slice.toArray.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  (s : Std.Slice γ), s.toArray = (Std.Slice.Internal.iter s).toArray
-- Mathlib.Algebra.Module.SpanRankOperations
IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R],
  (IsLocalRing.maximalIdeal R).FG →
    Submodule.spanFinrank (IsLocalRing.maximalIdeal R) =
      Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.instNonemptyOfObjOfNonempty : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) [Nonempty ι],
  (CategoryTheory.ObjectProperty.ofObj X).Nonempty
-- Mathlib.NumberTheory.FLT.Basic
fermatLastTheoremFor_iff_int : ∀ {n : ℕ}, FermatLastTheoremFor n ↔ FermatLastTheoremWith ℤ n
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_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.kahler x) x = ↑‖x‖ ^ 2
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weight_comp : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : {i j : V} → (i ⟶ j) → R) {a b c : V}
  (p : Quiver.Path a b) (q : Quiver.Path b c),
  Quiver.Path.weight (fun {i j} => w) (p.comp q) =
    Quiver.Path.weight (fun {i j} => w) p * Quiver.Path.weight (fun {i j} => w) q
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.ofQuotientStabilizer_mem_orbit : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (x : X) (g : G ⧸ AddAction.stabilizer G x),
  AddAction.ofQuotientStabilizer G x g ∈ AddAction.orbit G x
-- Mathlib.Analysis.Matrix.Order
Matrix.PosSemidef.inv_sqrt : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜},
  A.PosSemidef → (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Structure for representing monomials with coefficients.  -/
Tactic.ComputeAsymptotics.Monomial : Type
-- Mathlib.FieldTheory.Finite.Basic
ZMod.card_units : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Fintype.card (ZMod p)ˣ = p - 1
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.smul_mem_iff' : ∀ {G : Type u''} {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {x : M} [inst_2 : Group G] [inst_3 : MulAction G M] [inst_4 : SMul G R] [IsScalarTower G R M]
  (g : G), g • x ∈ p ↔ x ∈ p
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_mem_nhdsSet : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α) {δ : ℝ}, 0 < δ → Metric.thickening δ E ∈ nhdsSet E
-- Mathlib.Dynamics.Ergodic.Action.Basic
ergodicSMul_iff : ∀ (G : Type u_1) (α : Type u_2) [inst : SMul G α] {x : MeasurableSpace α} (μ : MeasureTheory.Measure α),
  ErgodicSMul G α μ ↔
    MeasureTheory.SMulInvariantMeasure G α μ ∧
      ∀ {s : Set α},
        MeasurableSet s → (∀ (g : G), (fun x => g • x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Init.System.ST
EST.Out.ok.injEq : ∀ {ε σ α : Type} (a : α) (a_1 : Void σ) (a_2 : α) (a_3 : Void σ),
  (EST.Out.ok a a_1 = EST.Out.ok a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Data.Set.Function
Set.mapsTo_inter : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.MapsTo f s (t₁ ∩ t₂) ↔ Set.MapsTo f s t₁ ∧ Set.MapsTo f s t₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  {l : List ((a : α) × β a)}, m.WF → (m.insertMany l).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) m l)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.toComonObj : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {M : C} → [self : CategoryTheory.BimonObj M] → CategoryTheory.ComonObj M
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.nsmul : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x ≡ y [SMOD U] → ∀ (n : ℕ), n • x ≡ n • y [SMOD U]
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the preimage of `perfectClosure F K`
under the map `i` is equal to `perfectClosure F E`.  -/
perfectClosure.comap_eq_of_algHom : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E →ₐ[F] K), IntermediateField.comap i (perfectClosure F K) = perfectClosure F E
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SupSet γ]
  [inst_3 : SupSet δ] (f : sSupHom γ δ) (g : sSupHom β γ) (h : sSupHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_of_not_isPrime : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S],
  ¬q.IsPrime → q.ramificationIdx R = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getInst? : Lean.Name → Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.FieldTheory.KummerExtension
AdjoinRootXPowSubCEquivToRootsOfUnity.congr_simp : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [inst_1 : NeZero n]
  (σ σ_1 : AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)),
  σ = σ_1 → AdjoinRootXPowSubCEquivToRootsOfUnity hζ H σ = AdjoinRootXPowSubCEquivToRootsOfUnity hζ H σ_1
-- Mathlib.Topology.Category.CompHaus.Basic
CompHaus.instCoeSortType : CoeSort CompHaus (Type u_1)
-- Init.Tactics
/-- `refine' e` behaves like `refine e`, except that unsolved placeholders (`_`)
and implicit parameters are also converted into new goals.
 -/
Lean.Parser.Tactic.refine' : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.inner_real_eq_re_inner : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (x y : H), inner ℝ x y = (inner ℂ x y).re
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMin'.eq_1 : ∀ {α : Type u_1} (x : α), Ordnode.nil.findMin' x = x
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The underlying morphism of the forward component of the left unitor isomorphism.  -/
Bimod.LeftUnitorBimod.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        {R S : CategoryTheory.Mon C} → (P : Bimod R S) → Bimod.TensorBimod.X (Bimod.regular R) P ⟶ P.X
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.subalgebra.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B),
  Algebra.Smooth.DescentAux.subalgebra✝ R D =
    Algebra.adjoin R
      ((Algebra.Smooth.DescentAux.P✝ D).coeffs ∪
        (((⋃ i, ↑(Algebra.Smooth.DescentAux.h✝ D i).coeffs) ∪
            ⋃ i, ⋃ x ∈ (Algebra.Smooth.DescentAux.q✝ D i).coeffs, ↑(MvPolynomial.coeffs x)) ∪
          ⋃ i, ⋃ x ∈ (Algebra.Smooth.DescentAux.p✝ D i).coeffs, ↑x.coeffs))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.isShared.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_25) (fvarId_1 : Lean.FVarId)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_25),
  (Lean.Compiler.LCNF.LetValue.isShared fvarId h = Lean.Compiler.LCNF.LetValue.isShared fvarId_1 h_1) =
    (fvarId = fvarId_1)
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).i = CategoryTheory.Limits.kernel.ι S.g
-- Mathlib.Topology.SmallInductiveDimension
HasSmallInductiveDimensionLT.succ : ∀ {X : Type u} [inst : TopologicalSpace X] (n : ℕ) (s : Set (Set X)),
  TopologicalSpace.IsTopologicalBasis s →
    (∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) n) → HasSmallInductiveDimensionLT X (n + 1)
-- Mathlib.Algebra.Azumaya.Matrix
/-- A nontrivial matrix ring over `R` is an Azumaya algebra over `R`.  -/
IsAzumaya.matrix : ∀ (R : Type u_1) (n : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] [Nonempty n],
  IsAzumaya R (Matrix n n R)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.projKerOfRightInverse.congr_simp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Ring R₁] [inst_1 : Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_4} {M₂ : Type u_5} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : Module R₁ M₁] [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommGroup M₂]
  [inst_8 : Module R₂ M₂] [inst_9 : IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ f₂_1 : M₂ →SL[σ₂₁] M₁)
  (e_f₂ : f₂ = f₂_1) (h : Function.RightInverse ⇑f₂ ⇑f₁),
  f₁.projKerOfRightInverse f₂ h = f₁.projKerOfRightInverse f₂_1 ⋯
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.Nonempty.of_sdiff`. -/
Set.Nonempty.of_diff : ∀ {α : Type u} {s t : Set α}, (s \ t).Nonempty → s.Nonempty
-- Mathlib.GroupTheory.Finiteness
/-- In a canonically ordered and well-quasi-ordered monoid, any divisive submonoid is finitely
generated.  -/
Submonoid.fg_of_divisive : ∀ {M : Type u_5} [inst : CommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelMonoid M]
  [CanonicallyOrderedMul M] {P : Submonoid M}, (∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P) → P.FG
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.zsmul_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddGroup (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (i : ι)
  (x : G i) (n : ℤ), n • ⟦⟨i, x⟩⟧ = ⟦⟨i, n • x⟩⟧
-- Mathlib.Analysis.Analytic.Binomial
/-- `∑ (ai + b) zⁱ = (b - a) / (1 - z) + a / (1 - z)²`  -/
Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero : ∀ (a b : ℝ),
  HasFPowerSeriesOnBall (fun x => (b - a) / (1 - x) + a / (1 - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℝ fun x => a * ↑x + b) 0 1
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.IsRingHom.toIsAddMonHom : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {R₁ R₂ : C} {inst_2 : CategoryTheory.AddMonObj R₁} {inst_3 : CategoryTheory.AddMonObj R₂}
  {inst_4 : CategoryTheory.MonObj R₁} {inst_5 : CategoryTheory.MonObj R₂} {f : R₁ ⟶ R₂}
  [self : CategoryTheory.IsRingHom f], CategoryTheory.IsAddMonHom f
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailESTOfNonempty : {ε σ : Type} → [Nonempty ε] → Lean.Order.MonadTail (EST ε σ)
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_pair : ∀ (x y : ZFSet.{u_1}), {x, y}.rank = max (Order.succ x.rank) (Order.succ y.rank)
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.mk.inj : ∀ {D : Type u_5} {inst : CategoryTheory.Category.{v_5, u_5} D} {M : Type u_6} {inst_1 : AddCommMonoid M}
  {inst_2 : CategoryTheory.HasShift D M}
  {toTwistShiftData :
    CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M))
      (M × M)}
  {z_zero₁ :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (0, m₁) (0, m₂) = 1) CategoryTheory.CommShift₂Setup.z_zero₁._autoParam}
  {z_zero₂ :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (m₁, 0) (m₂, 0) = 1) CategoryTheory.CommShift₂Setup.z_zero₂._autoParam}
  {ε : M → M → (CategoryTheory.CatCenter D)ˣ}
  {hε :
    autoParam (∀ (m n : M), ε m n = (toTwistShiftData.z (0, n) (m, 0))⁻¹ * toTwistShiftData.z (m, 0) (0, n))
      CategoryTheory.CommShift₂Setup.hε._autoParam}
  {toTwistShiftData_1 :
    CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M))
      (M × M)}
  {z_zero₁_1 :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData_1.z (0, m₁) (0, m₂) = 1)
      CategoryTheory.CommShift₂Setup.z_zero₁._autoParam}
  {z_zero₂_1 :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData_1.z (m₁, 0) (m₂, 0) = 1)
      CategoryTheory.CommShift₂Setup.z_zero₂._autoParam}
  {ε_1 : M → M → (CategoryTheory.CatCenter D)ˣ}
  {hε_1 :
    autoParam (∀ (m n : M), ε_1 m n = (toTwistShiftData_1.z (0, n) (m, 0))⁻¹ * toTwistShiftData_1.z (m, 0) (0, n))
      CategoryTheory.CommShift₂Setup.hε._autoParam},
  { toTwistShiftData := toTwistShiftData, z_zero₁ := z_zero₁, z_zero₂ := z_zero₂, ε := ε, hε := hε } =
      { toTwistShiftData := toTwistShiftData_1, z_zero₁ := z_zero₁_1, z_zero₂ := z_zero₂_1, ε := ε_1, hε := hε_1 } →
    toTwistShiftData = toTwistShiftData_1 ∧ ε = ε_1
-- Mathlib.Order.Comparable
AntisymmRel.compRel : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, AntisymmRel r a b → CompRel r a b
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.«term_∘₂_» : Lean.TrailingParserDescr
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Entry.measure.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (k : α) (v : β), (Lean.PersistentHashMap.Entry.entry k v).measure = 1
-- Mathlib.Computability.Primrec.Basic
/-- `PrimrecRel p` means `p : α → β → Prop` is a
primitive recursive relation, which is to say that
`decide ∘ p : α → β → Bool` is primitive recursive.  -/
PrimrecRel : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → (α → β → Prop) → Prop
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (toContinuousMap : C(α, β))
  (cocompact_tendsto' : Filter.Tendsto toContinuousMap.toFun (Filter.cocompact α) (Filter.cocompact β))
  (toContinuousMap_1 : C(α, β))
  (cocompact_tendsto'_1 : Filter.Tendsto toContinuousMap_1.toFun (Filter.cocompact α) (Filter.cocompact β)),
  ({ toContinuousMap := toContinuousMap, cocompact_tendsto' := cocompact_tendsto' } =
      { toContinuousMap := toContinuousMap_1, cocompact_tendsto' := cocompact_tendsto'_1 }) =
    (toContinuousMap = toContinuousMap_1)
-- Mathlib.Data.Stream.Init
Stream'.inits_core_eq : ∀ {α : Type u} (l : List α) (s : Stream' α),
  Stream'.initsCore l s = Stream'.cons l (Stream'.initsCore (l ++ [s.head]) s.tail)
-- Mathlib.Analysis.Calculus.DSlope
DifferentiableOn.of_dslope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜}, DifferentiableOn 𝕜 (dslope f a) s → DifferentiableOn 𝕜 f s
-- Lean.Data.Lsp.Window
Lean.Lsp.instToJsonShowMessageParams.toJson : Lean.Lsp.ShowMessageParams → Lean.Json
-- Init.Data.BitVec.Lemmas
BitVec.xor_zero : ∀ {w : ℕ} {x : BitVec w}, x ^^^ 0#w = x
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.not_isStrongPrelimit_iff : ∀ {c : Cardinal.{u_1}}, ¬c.IsStrongPrelimit ↔ ∃ x < c, c ≤ 2 ^ x
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.coeAddMonoidHom_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (self : ↥I), I.coeAddMonoidHom self = ↑self
-- Mathlib.Topology.EMetricSpace.Defs
edist_toDual : ∀ {X : Type u_1} [inst : EDist X] (a b : X), edist (OrderDual.toDual a) (OrderDual.toDual b) = edist a b
-- Mathlib.Algebra.Group.ULift
ULift.add_down : ∀ {α : Type u} {x y : ULift.{w, u} α} [inst : Add α], (x + y).down = x.down + y.down
-- Mathlib.Analysis.Calculus.AddTorsor.AffineMap
ContDiffWithinAt.lineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₁ f₂ : E → V} {g : E → 𝕜}
  {s : Set E} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f₁ s x →
    ContDiffWithinAt 𝕜 n f₂ s x →
      ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s x
-- Mathlib.Algebra.Algebra.RestrictScalars
RestrictScalars.ringEquiv_map_smul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_4) [inst : Semiring A] [inst_1 : CommSemiring S] [inst_2 : Algebra S A]
  [inst_3 : CommSemiring R] [inst_4 : Algebra R S] (r : R) (x : RestrictScalars R S A),
  (RestrictScalars.ringEquiv R S A) (r • x) = (algebraMap R S) r • (RestrictScalars.ringEquiv R S A) x
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
InnerProductSpace.volume_ball_of_dim_even : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [Nontrivial E] {k : ℕ},
  Module.finrank ℝ E = 2 * k →
    ∀ (x : E) (r : ℝ),
      MeasureTheory.volume (Metric.ball x r) =
        ENNReal.ofReal r ^ Module.finrank ℝ E * ENNReal.ofReal (Real.pi ^ k / ↑k.factorial)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_pullback₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f],
  (CategoryTheory.PreZeroHypercover.pullback₂ f E).presieve₀ = CategoryTheory.Presieve.pullbackArrows f E.presieve₀
-- Init.System.IO
/-- Returns the current thread's standard input stream.

Use `IO.setStdin` to replace the current thread's standard input stream.
 -/
IO.getStdin : BaseIO IO.FS.Stream
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- If a finset `u` is contained in the pointwise subtraction of two sets `s -ᵥ t`, we can find two
finsets `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' -ᵥ t'`.  -/
Finset.subset_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {u : Finset α} {s t : Set β},
  ↑u ⊆ s -ᵥ t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' -ᵥ t'
-- Mathlib.Analysis.Convex.Extreme
extremePoints_convexHull_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E] {A : Set E},
  Set.extremePoints 𝕜 ((convexHull 𝕜) A) ⊆ A
-- Init.GrindInstances.Ring.UInt
UInt16.ofInt.eq_1 : ∀ (x : ℤ), UInt16.ofInt x = UInt16.ofNat (x % 2 ^ 16).toNat
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {s : Set 𝕜}, Meromorphic f → MeromorphicOn f s