mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Date.Unit.Weekday
Std.Time.instReprWeekday.repr : Std.Time.Weekday → ℕ → Std.Format
-- Init.Data.String.Defs
String.append_singleton : ∀ {s : String} {c : Char}, s ++ String.singleton c = s.push c
-- Init.Prelude
/-- Updates the current state with the saved information that should be rolled back. This updated
state becomes the current state when an exception is handled.
 -/
EStateM.Backtrackable.restore : {δ : outParam (Type u)} → {σ : Type u} → [self : EStateM.Backtrackable δ σ] → σ → δ → σ
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.OptionT.bind.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.instAddCommMonoid : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → AddCommMonoid (WeakDual 𝕜 E)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.instReprKey.repr : Lean.Meta.DiscrTree.Key → ℕ → Std.Format
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The line derivative in direction `m` of the inverse Fourier transform is given by the inverse
Fourier transform of the multiplication with `(2 * π * Complex.I) • (inner ℝ · m)`.  -/
TemperedDistribution.lineDerivOp_fourierInv_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] (f : TemperedDistribution E F) (m : E),
  LineDeriv.lineDerivOp m (FourierTransformInv.fourierInv f) =
    FourierTransformInv.fourierInv
      ((2 * ↑Real.pi * Complex.I) • (TemperedDistribution.smulLeftCLM F fun x => ↑(inner ℝ x m)) f)
-- Mathlib.Computability.RecursiveIn
/-- If a partial function is partial recursive, then it is `RecursiveIn` any oracle set.  -/
Partrec.recursiveIn : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ} {O : Set (ℕ →. ℕ)},
  Partrec f → RecursiveIn O f
-- Lean.Meta.Tactic.Simp.Types
/-- Given the application `e`, remove unnecessary casts of the form `Eq.rec a rfl` and `Eq.ndrec a rfl`.  -/
Lean.Meta.Simp.removeUnnecessaryCasts : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_C : ∀ {R : Type u_1} [inst : Semiring R] (r x : R), (Polynomial.taylor r) (Polynomial.C x) = Polynomial.C x
-- Batteries.Data.List.Basic
List.headD_eq_head? : ∀ {α : Type u_1} (l : List α) (a : α), l.headD a = l.head?.getD a
-- Std.Time.Zoned.RecurringRule
/-- Returns the `Day.Offset` (days since epoch) for a `TransitionSpec.mwd` in the given year.

`Mm.w.d`: month `m`, week `w` (1–5; 5 = last), ISO weekday `d` (1 = Monday, 7 = Sunday).
Finds the `w`-th occurrence of weekday `d` in month `m`; if `w = 5`, returns the last occurrence.
 -/
Std.Time.TimeZone.TransitionSpec.toEpochDayMWD : Std.Time.Year.Offset →
  Std.Time.Month.Ordinal → Std.Time.Week.Aligned.Ordinal → Std.Time.Weekday.Ordinal → Std.Time.Day.Offset
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eraseKey_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    (a == k) = true → Std.Internal.List.containsKey a (Std.Internal.List.eraseKey k l) = false
-- Init.Data.Vector.Lemmas
Vector.reverse_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m},
  (xs ++ ys).reverse = Vector.cast ⋯ (ys.reverse ++ xs.reverse)
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- The set of periodic points of a map `f : α → α`.  -/
Function.periodicPts : {α : Type u_1} → (α → α) → Set α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.forIn_eq_forIn_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toArray init f
-- Mathlib.Order.Category.BddLat
BddLat.Iso.mk_hom : ∀ {α β : BddLat} (e : ↑α.toLat ≃o ↑β.toLat),
  (BddLat.Iso.mk e).hom =
    BddLat.ofHom
      (have __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- **Alias** of `ciInf_subtype_fun`. -/
ciInf_subtype'' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_5} {s : Set ι} {f : ι → α},
  BddBelow (Set.range fun i => f ↑i) → ⨅ i, f ↑i ≤ sInf ∅ → ⨅ i, f ↑i = ⨅ t ∈ s, f t
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
FiberBundle.contMDiffAt_extend : ∀ {𝕜 : 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] (F : Type u_5) [inst_6 : NormedAddCommGroup F]
  {V : M → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → AddCommGroup (V x)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : NormedSpace 𝕜 F] {k : WithTop ℕ∞}
  {x : M} (σ₀ : V x), ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x' => ⟨x', FiberBundle.extend F σ₀ x'⟩) x
-- Init.Data.Iterators.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_1.eq_1 : ∀ {β : Type u_3} (γ : Type u_1) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (acc : γ) (out : β)
  (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) (c : γ)
  (h' : PlausibleForInStep out acc (ForInStep.yield c))
  (h_1 : (c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩)
  (h_2 : (c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩),
  (match ⟨ForInStep.yield c, h'⟩ with
    | ⟨ForInStep.yield c, h'⟩ => h_1 c h'
    | ⟨ForInStep.done c, h⟩ => h_2 c h) =
    h_1 c h'
-- Init.Data.Prod
Prod.instLawfulBEq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β] [LawfulBEq α] [LawfulBEq β], LawfulBEq (α × β)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.instQuiver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  Quiver (F.DescentData' sq sq₃)
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctorMapObj_ext_iff : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {I : Type u_4} {J : Type u_5} {K : Type u_6}
  {p : I × J → K} {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K}
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
  {f g : CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k ⟶ A},
  f = g ↔
    ∀ (i : I) (j : J) (hij : p (i, j) = k),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) g
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_τ₂ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  (groupCohomology.mapShortComplexH2 f φ).τ₂ = groupCohomology.cochainsMap₂ f φ
-- Init.Grind.Interactive
/-- `skip` does nothing.  -/
Lean.Parser.Tactic.Grind.skip : Lean.ParserDescr
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- If `p` and `q` are distinct primes that are both congruent to `3` mod `4`, then `q` is
a square mod `p` iff `p` is a nonsquare mod `q`.  -/
ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three : ∀ {p q : ℕ} [inst : Fact (Nat.Prime p)] [inst_1 : Fact (Nat.Prime q)],
  p % 4 = 3 → q % 4 = 3 → p ≠ q → (IsSquare ↑q ↔ ¬IsSquare ↑p)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctorPreCore B C) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
  self.map₂ (CategoryTheory.Bicategory.whiskerRight η g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The underlying `Mor₂` term of a `HorizontalComp` term.  -/
Mathlib.Tactic.BicategoryLike.HorizontalComp.e : Mathlib.Tactic.BicategoryLike.HorizontalComp → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Tactic.Linter.TextBased
/-- Context for a style error: the actual error, the line number in the file we're reading
and the path to the file.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext : Type
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = (t.getKey? a).isSome
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.preservesEpimorphisms_comp : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.PreservesEpimorphisms] [G.PreservesEpimorphisms], (F.comp G).PreservesEpimorphisms
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k fallback : α}, (Std.TreeMap.map f t).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Algebra.Group.Units.Basic
unique_zero : ∀ {α : Type u_1} [inst : Unique α] [inst_1 : Zero α], default = 0
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasStrictFDerivAt.isTheta_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → Topology.IsInducing ⇑f' → (fun p => f p.1 - f p.2) =Θ[nhds (x, x)] fun p => p.1 - p.2
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.homObjFunctor_obj : ∀ {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) (A : (CategoryTheory.Functor C (Type w))ᵒᵖ),
  (F.homObjFunctor G).obj A = F.HomObj G (Opposite.unop A)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulHom.eq_1 : @Pi.mulHom = @MulHom.pi
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.insertListIfNew.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l toInsert : List ((a : α) × β a)),
  Std.Internal.List.insertListIfNew l toInsert =
    match toInsert with
    | [] => l
    | ⟨k, v⟩ :: tl => Std.Internal.List.insertListIfNew (Std.Internal.List.insertEntryIfNew k v l) tl
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.norm_approxOn_y₀_le : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [inst_3 : OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s)
  [inst_4 : TopologicalSpace.SeparableSpace ↑s] (x : β) (n : ℕ),
  ‖(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.sum_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α), σ.cycleType.sum = σ.support.card
-- Lean.SubExpr
Lean.SubExpr.Pos.tail : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntry.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : x.isEmpty = false) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (l : Std.DTreeMap.Internal.Impl α β) →
                    (x :
                        (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β k_1) →
                            (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                              (h :
                                  (Std.DTreeMap.Internal.Impl.inner size k v l
                                        (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
                                    false) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v l
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                  h) →
              motive x x_1
-- Mathlib.Order.InitialSeg
PrincipalSeg.codRestrict_top : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (p : Set β) (f : PrincipalSeg r s)
  (H : ∀ (a : α), f.toRelEmbedding a ∈ p) (H₂ : f.top ∈ p), (PrincipalSeg.codRestrict p f H H₂).top = ⟨f.top, H₂⟩
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_iff : ∀ {p : ℕ}, Nat.Prime p ↔ Prime p
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.instInhabitedFixedParamPerms : Inhabited Lean.Elab.FixedParamPerms
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd_lt_oadd_3 : ∀ {e : ONote} {n : ℕ+} {a₁ a₂ : ONote}, a₁ < a₂ → e.oadd n a₁ < e.oadd n a₂
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens),
  AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯))
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.formPerm_toList : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α) (x : α),
  (f.toList x).formPerm = f.cycleOf x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α) (v : β k), (t₁.insert k v).Equiv (t₂.insert k v)
-- Init.Data.SInt.Basic
/-- Obtains the `Int64` that is 2's complement equivalent to the `UInt64`.  -/
UInt64.toInt64 : UInt64 → Int64
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_apply : ∀ {R : Type u_1} [inst : Semiring R] (k : ℕ) (f : Polynomial R),
  (Polynomial.hasseDeriv k) f = f.sum fun i r => (Polynomial.monomial (i - k)) (↑(i.choose k) * r)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.intCast.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (n : ℤ),
  Lean.Grind.Ring.OfSemiring.intCast n =
    if n < 0 then Lean.Grind.Ring.OfSemiring.Q.mk (0, ↑n.natAbs) else Lean.Grind.Ring.OfSemiring.Q.mk (↑n.natAbs, 0)
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.BoundedAtFilter.mul : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedRing β] {l : Filter α} {f g : α → β},
  l.BoundedAtFilter f → l.BoundedAtFilter g → l.BoundedAtFilter (f * g)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instCategoryProfiniteGrp.eq_1 : instCategoryProfiniteGrp =
  { Hom := fun A B => A.Hom B, id := fun A => { hom' := ContinuousMonoidHom.id ↑A.toProfinite.toTop },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @instCategoryProfiniteGrp._proof_1,
    comp_id := @instCategoryProfiniteGrp._proof_2, assoc := @instCategoryProfiniteGrp._proof_3 }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂₃.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  h.p₂₃ = h.chosenPullback.p₂
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_balanceRErase : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size),
  (Std.DTreeMap.Internal.Impl.balanceRErase k v l r hlb hrb hlr).Balanced
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optEllipsis.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Array.Lemmas
Array.size_filter_pos_iff : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, 0 < (Array.filter p xs).size ↔ ∃ x ∈ xs, p x = true
-- Lean.Meta.Basic
Lean.Meta.ConfigWithKey.key : Lean.Meta.ConfigWithKey → UInt64
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.norm_changeOriginSeriesTerm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l),
  ‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.extendScalars.congr_simp : ∀ {R : Type u} (S : Type v) {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_2}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  (P P_1 : Algebra.Generators R T ι),
  P = P_1 → Algebra.Generators.extendScalars S P = Algebra.Generators.extendScalars S P_1
-- Mathlib.Data.Rel
SetRel.exists_eq_singleton_of_prod_subset_id : ∀ {α : Type u_1} {s t : Set α}, s.Nonempty → t.Nonempty → s ×ˢ t ⊆ SetRel.id → ∃ x, s = {x} ∧ t = {x}
-- Mathlib.Data.Set.Defs
/-- The difference of two sets `s` and `t` is the set of elements contained in `s` but not in `t`.

Note that you should **not** use this definition directly, but instead write `s \ t`.  -/
Set.diff : {α : Type u} → Set α → Set α → Set α
-- Init.Grind.Config
Lean.Grind.ConfigInteractive.mk : Lean.Grind.Config → Lean.Grind.ConfigInteractive
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.RespectsIso.of_iso : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.RespectsIso]
  {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F),
  E.presieve₀ ∈ J.coverings S → F.presieve₀ ∈ J.coverings S
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.congr_of_mem : ∀ {𝕜 : 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'} {s : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → (∀ y ∈ s, f₁ y = f y) → x ∈ s → ContMDiffWithinAt I I' n f₁ s x
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.pullbackPushforwardAdjunction.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y), TopCat.Presheaf.pullbackPushforwardAdjunction C f = (TopologicalSpace.Opens.map f).op.lanAdjunction C
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Typecheck a morphism in `ForgetEnrichment W C` as a `(𝟙_ W)`-shaped `W`-morphism.  -/
CategoryTheory.ForgetEnrichment.homTo : {C : Type u₁} →
  (W : Type v) →
    [inst : CategoryTheory.Category.{w, v} W] →
      [inst_1 : CategoryTheory.MonoidalCategory W] →
        [inst_2 : CategoryTheory.EnrichedCategory W C] →
          {X Y : CategoryTheory.ForgetEnrichment W C} →
            (X ⟶ Y) →
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶
                CategoryTheory.ForgetEnrichment.to W X ⟶[W] CategoryTheory.ForgetEnrichment.to W Y)
-- Mathlib.RingTheory.Invariant.Profinite
Algebra.IsInvariant.isIntegral_of_profinite : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {G : Type u}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [SMulCommClass G A B] [inst_6 : TopologicalSpace G]
  [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [inst_10 : TopologicalSpace B]
  [DiscreteTopology B] [ContinuousSMul G B] [Algebra.IsInvariant A B G], Algebra.IsIntegral A B
-- Lean.Elab.ConfigEval.Commands
Lean.Elab.ConfigEval.configEntryHandlerKeyWildcard : Lean.ParserDescr
-- Mathlib.Algebra.Order.BigOperators.Ring.Multiset
CanonicallyOrderedAdd.multiset_prod_pos : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R]
  [Nontrivial R] {m : Multiset R}, 0 < m.prod ↔ ∀ x ∈ m, 0 < x
-- Mathlib.Dynamics.Ergodic.Conservative
MeasureTheory.conservative_congr : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ ν : MeasureTheory.Measure α},
  MeasureTheory.ae μ = MeasureTheory.ae ν → (MeasureTheory.Conservative f μ ↔ MeasureTheory.Conservative f ν)
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix.congr_simp : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : Zero α]
  [inst_3 : One α] (f f_1 : m ≃. n),
  f = f_1 → ∀ (a a_1 : m), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → f.toMatrix a a_2 = f_1.toMatrix a_1 a_3
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The scalar action via `mul.toOppositeSMul` is transformed by the same map as the
elements of the matrix, when `f` preserves multiplication.  -/
Matrix.map_op_smul' : ∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : Mul α] [inst_1 : Mul β] (f : α → β) (r : α) (A : Matrix n n α),
  (∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) → (MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f