mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.mk.injEq : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} {B : Type w} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (toCoalgEquiv : A ≃ₗc[R] B)
  (map_mul' : ∀ (x y : A), toCoalgEquiv.toFun (x * y) = toCoalgEquiv.toFun x * toCoalgEquiv.toFun y)
  (toCoalgEquiv_1 : A ≃ₗc[R] B)
  (map_mul'_1 : ∀ (x y : A), toCoalgEquiv_1.toFun (x * y) = toCoalgEquiv_1.toFun x * toCoalgEquiv_1.toFun y),
  ({ toCoalgEquiv := toCoalgEquiv, map_mul' := map_mul' } =
      { toCoalgEquiv := toCoalgEquiv_1, map_mul' := map_mul'_1 }) =
    (toCoalgEquiv = toCoalgEquiv_1)
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_pow_eq_iterate : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : Monoid F'] [IsMulApplyEqComp F' α]
  [IsOneApplyEqSelf F' α] (f : F') (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.Topology.MetricSpace.Similarity
/-- **Alias** of `similar_of_dist_mul_eq_dist_mul_eq`.

---

If two triangles have two pairs of proportional adjacent sides, then the triangles are similar.
 -/
similar_of_side_side : ∀ {P₁ : Type u_3} {P₂ : Type u_4} [inst : PseudoMetricSpace P₁] [inst_1 : PseudoMetricSpace P₂] {a b c : P₁}
  {a' b' c' : P₂},
  dist a b ≠ 0 →
    dist a' b' ≠ 0 →
      dist a b * dist b' c' = dist b c * dist a' b' →
        dist a b * dist c' a' = dist c a * dist a' b' → Similar ![a, b, c] ![a', b', c']
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- Assemble an algebra morphism `TrivSqZeroExt R M →ₐ[S] A` from separate morphisms on `R` and `M`.

Namely, we require that for an algebra morphism `f : R →ₐ[S] A` and a linear map `g : M →ₗ[S] A`,
we have:

* `g x * g y = 0`: the elements of `M` continue to square to zero.
* `g (r •> x) = f r * g x` and `g (x <• r) = g x * f r`: scalar multiplication on the left and
  right is sent to left- and right- multiplication by the image under `f`.

See `TrivSqZeroExt.liftEquiv` for this as an equiv; namely that any such algebra morphism can be
factored in this way.

When `R` is commutative, this can be invoked with `f = Algebra.ofId R A`, which satisfies `hfg` and
`hgf`. This version is captured as an equiv by `TrivSqZeroExt.liftEquivOfComm`.  -/
TrivSqZeroExt.lift : {S : Type u_1} →
  {R : Type u} →
    {M : Type v} →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra S R] →
              [inst_4 : Module S M] →
                [inst_5 : Module R M] →
                  [inst_6 : Module Rᵐᵒᵖ M] →
                    [inst_7 : SMulCommClass R Rᵐᵒᵖ M] →
                      [inst_8 : IsScalarTower S R M] →
                        [inst_9 : IsScalarTower S Rᵐᵒᵖ M] →
                          {A : Type u_2} →
                            [inst_10 : Semiring A] →
                              [inst_11 : Algebra S A] →
                                (f : R →ₐ[S] A) →
                                  (g : M →ₗ[S] A) →
                                    (∀ (x y : M), g x * g y = 0) →
                                      (∀ (r : R) (x : M), g (r • x) = f r * g x) →
                                        (∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) →
                                          TrivSqZeroExt R M →ₐ[S] A
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.ext : Lean.SimpleScopedEnvExtension Lean.Compiler.CSimp.Entry Lean.Compiler.CSimp.State
-- Std.Data.Iterators.Lemmas.Consumers.Set
Std.IterM.toExtHashSet.congr_simp : ∀ {α β : Type w} [inst : BEq β] [inst_1 : Hashable β] [inst_2 : EquivBEq β] [inst_3 : LawfulHashable β]
  {m : Type w → Type w'} [inst_4 : Monad m] [inst_5 : Std.Iterator α m β] [inst_6 : Std.IteratorLoop α m m]
  (it it_1 : Std.IterM m β), it = it_1 → it.toExtHashSet = it_1.toExtHashSet
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁), CategoryTheory.Mono ((F.shift n₁).map T.mor₁) ↔ F.homologySequenceδ T n₀ n₁ h = 0
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr : ∀ (m n : ℕ) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m) (rhs' : BitVec n),
  lhs' = lhs → rhs' = rhs → lhs <<< rhs = lhs' <<< rhs'
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instSMulZeroClassQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : Zero M] →
      [inst_1 : Add M] → [inst_2 : SMulZeroClass S M] → (c : ModuleCon S M) → SMulZeroClass S (ModuleCon.Quotient M c)
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go.match_1.eq_6 : ∀ (motive : Lean.Level → Lean.Level → Sort u_1) (x x_1 : Lean.Level) (h_1 : (x : Lean.Level) → motive x Lean.Level.zero)
  (h_2 : (u v₁ v₂ : Lean.Level) → motive u (v₁.max v₂)) (h_3 : (u₁ u₂ v : Lean.Level) → motive (u₁.max u₂) v)
  (h_4 : (a u₂ v : Lean.Level) → motive (a.imax u₂) v) (h_5 : (u v : Lean.Level) → motive u.succ v.succ)
  (h_6 : (x x_2 : Lean.Level) → motive x x_2),
  (x_1 = Lean.Level.zero → False) →
    (∀ (v₁ v₂ : Lean.Level), x_1 = v₁.max v₂ → False) →
      (∀ (u₁ u₂ : Lean.Level), x = u₁.max u₂ → False) →
        (∀ (a u₂ : Lean.Level), x = a.imax u₂ → False) →
          (∀ (u v : Lean.Level), x = u.succ → x_1 = v.succ → False) →
            (match x, x_1 with
              | x, Lean.Level.zero => h_1 x
              | u, v₁.max v₂ => h_2 u v₁ v₂
              | u₁.max u₂, v => h_3 u₁ u₂ v
              | a.imax u₂, v => h_4 a u₂ v
              | u.succ, v.succ => h_5 u v
              | x, x_7 => h_6 x x_7) =
              h_6 x x_1
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instMulLeftReflectLT : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Mul α] [MulLeftReflectLT α], MulLeftReflectLT (WithZero α)
-- Batteries.Data.PairingHeap
/-- A node containing a single element `a`.  -/
Batteries.PairingHeapImp.Heap.singleton : {α : Type u_1} → α → Batteries.PairingHeapImp.Heap α
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The entire function differing from `completedCosZeta a s` by a linear combination of
`1 / s` and `1 / (1 - s)`.  -/
HurwitzZeta.completedCosZeta₀ : UnitAddCircle → ℂ → ℂ
-- Init.Data.List.MinMaxOn
List.maxOn?_replicate_of_pos : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {n : ℕ} {a : α}
  {f : α → β}, 0 < n → List.maxOn? f (List.replicate n a) = some a
-- Mathlib.Topology.Algebra.Group.Basic
continuousOn_zpow : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s : Set G} (z : ℤ),
  ContinuousOn (fun x => x ^ z) s
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The successor structure of the orthogonal-reflection construction.  -/
CategoryTheory.OrthogonalReflection.succStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      [inst_1 : CategoryTheory.Limits.HasPushouts C] →
        [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [∀ (Z : C),
                  CategoryTheory.Limits.HasMulticoequalizer
                    (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
              C → CategoryTheory.SmallObject.SuccStruct C
-- Mathlib.Algebra.Module.LinearMap.End
/-- See also `Module.End.natCast_def`.  -/
Module.End.natCast_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ) (m : M),
  ↑n m = n • m
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_degree_le_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.degree ≤ 0 → f.Splits
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_σ_comp_of_not_injective : ∀ {n : ℕ} {Δ' : SimplexCategory} (θ : { len := n + 1 } ⟶ Δ'),
  ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ) →
    ∃ i θ', θ = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) θ'
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balance!.match_3.eq_4 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α) (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (lrk : α) →
        (lrv : β lrk) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_4 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr with
    | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r => h_2 size lrk lrv l r
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_3 size k v l r
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
      h_4 size k v l r lrs lrk lrv lrl lrr) =
    h_4 size k v l r lrs lrk lrv lrl lrr
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- A function is continuous if and only if its composition with an open partial homeomorphism
on the left is continuous and its image is contained in the source.  -/
OpenPartialHomeomorph.continuous_iff_continuous_comp_left : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X},
  f ⁻¹' e.source = Set.univ → (Continuous f ↔ Continuous (↑e ∘ f))
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) f = CategoryTheory.CategoryStruct.id Y
-- Mathlib.Data.Multiset.Filter
Multiset.filter_le : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α), Multiset.filter p s ≤ s
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.zero_fst : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : AddCommGroup β], WithLp.fst 0 = 0
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.abstractLevels : Lean.Meta.AbstractMVars.State → Bool
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_eq_zero_iff : ∀ {a : ℤ} {n : ℕ}, a <<< n = 0 ↔ a = 0
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- Variant of the stereographic projection, for the sphere in an `n + 1`-dimensional inner product
space `E`.  This version has codomain the Euclidean space of dimension `n`, and is obtained by
composing the original stereographic projection (`stereographic`) with an arbitrary linear isometry
from `(ℝ ∙ v)ᗮ` to the Euclidean space.  -/
stereographic' : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      (n : ℕ) →
        [Fact (Module.finrank ℝ E = n + 1)] →
          ↑(Metric.sphere 0 1) → OpenPartialHomeomorph (↑(Metric.sphere 0 1)) (EuclideanSpace ℝ (Fin n))
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_sinh : Measurable Real.sinh
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_target_eq_image_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H}, (f.extend I).target = ↑(f.extend I) '' f.source
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.least_descending_central_series_length_eq_nilpotencyClass`.

---

The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which the descending
central series reaches `⊥` in its `n`-th term.  -/
least_descending_central_series_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedAddCommMonoid.toESeminormedAddMonoid : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ESeminormedAddCommMonoid E] → ESeminormedAddMonoid E
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_eq_map : ∀ {ι : Type u_1} (u : Set ι) (p : ↑unitInterval),
  ProbabilityTheory.setBernoulli u p =
    MeasureTheory.Measure.map (fun p => {i | p i})
      (MeasureTheory.Measure.infinitePi fun i =>
        unitInterval.toNNReal p • MeasureTheory.Measure.dirac (i ∈ u) +
          unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False)
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr),
  (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯
-- Init.Data.Ord.String
String.instLawfulEqOrd : Std.LawfulEqOrd String
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedExpr : Inhabited Lean.IR.Expr
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `le_mul_inv_iff₀'` for a version with multiplication on the other side.  -/
le_mul_inv_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (a ≤ b * c⁻¹ ↔ a * c ≤ b)
-- Mathlib.Topology.Connected.Basic
/-- A union of a family of preconnected sets with a common point is preconnected as well.  -/
isPreconnected_sUnion : ∀ {α : Type u} [inst : TopologicalSpace α] (x : α) (c : Set (Set α)),
  (∀ s ∈ c, x ∈ s) → (∀ s ∈ c, IsPreconnected s) → IsPreconnected (⋃₀ c)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.eq.sizeOf_spec : sizeOf Mathlib.Tactic.ITauto.AndKind.eq = 1
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.module : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Extension R S} → Module S P.Cotangent
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the smallest key.
 -/
Std.ExtDTreeMap.minKey : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → t ≠ ∅ → α
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.exactlyChars : Std.Internal.Parsec.String.Parser Char → ℕ → Std.Internal.Parsec.String.Parser String
-- Mathlib.CategoryTheory.Shift.Basic
/-- the shift by 0 identifies to the identity functor  -/
CategoryTheory.ShiftMkCore.zero : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] → (self : CategoryTheory.ShiftMkCore C A) → self.F 0 ≅ CategoryTheory.Functor.id C
-- Std.Http.Server.Connection
/-- Attempts a single non-blocking receive from the body and feeds any available chunk
into the machine, without going through the `Selectable.one` scheduler.

For fully-buffered bodies (e.g. `Body.Full`, `Body.Buffered`) this avoids one
`Selectable.one` round-trip when the chunk is already in memory. Streaming bodies
that have no producer waiting return `none` and fall through to the normal poll loop
unchanged.

Only one chunk is consumed here. Looping would introduce yield points between
`Body.tryRecv` calls, allowing a background producer to race ahead and close the
stream before `writeHead` runs — turning a streaming response with unknown size
into a fixed-length one.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.tryDrainBody : {β : Type} →
  [Std.Http.Body β] →
    Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving →
      β → Std.Async.Async (Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving × Option β)
-- Mathlib.Order.ModularLattice
/-- A weakly upper modular lattice is a lattice where `a ⊔ b` covers `a` and `b` if `a` and `b` both
cover `a ⊓ b`.  -/
IsWeakUpperModularLattice : (α : Type u_2) → [Lattice α] → Prop
-- Mathlib.Order.JordanHolder
CompositionSeries.Equivalent.smash : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ t₁ t₂ : CompositionSeries X}
  (hs : RelSeries.last s₁ = RelSeries.head s₂) (ht : RelSeries.last t₁ = RelSeries.head t₂),
  s₁.Equivalent t₁ →
    s₂.Equivalent t₂ → CompositionSeries.Equivalent (RelSeries.smash s₁ s₂ hs) (RelSeries.smash t₁ t₂ ht)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.named.injEq : ∀ (s s_1 : Lean.TSyntax `Lean.Parser.Term.namedArgument),
  (Lean.PrettyPrinter.Delaborator.AppImplicitArg.named s = Lean.PrettyPrinter.Delaborator.AppImplicitArg.named s_1) =
    (s = s_1)
-- Mathlib.Logic.Equiv.Prod
Equiv.prodProdProdComm_apply : ∀ (α : Type u_9) (β : Type u_10) (γ : Type u_11) (δ : Type u_12) (abcd : (α × β) × γ × δ),
  (Equiv.prodProdProdComm α β γ δ) abcd = ((abcd.1.1, abcd.2.1), abcd.1.2, abcd.2.2)
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_lt : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1]
  {m n : ℤ}, ↑m < ↑n ↔ m < n
-- Mathlib.Topology.Germ
/-- The value associated to a germ at a point. This is the common value
shared by all representatives at the given point.  -/
Filter.Germ.value : {X : Type u_4} → {α : Type u_5} → [inst : TopologicalSpace X] → {x : X} → (nhds x).Germ α → α
-- Mathlib.Data.Finset.Slice
Set.Sized.subsingleton' : ∀ {α : Type u_1} {A : Set (Finset α)} [inst : Fintype α], Set.Sized (Fintype.card α) A → A.Subsingleton
-- Lean.Elab.Term.TermElabM
/-- If `holesAsSyntheticOpaque` is `true`, then we mark metavariables associated
with `_`s as `syntheticOpaque` if they do not occur in patterns.
This option is useful when elaborating terms in tactics such as `refine'` where
we want holes there to become new goals. See issue #1681, we have
`refine' (fun x => _)
 -/
Lean.Elab.Term.Context.holesAsSyntheticOpaque : Lean.Elab.Term.Context → Bool
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- `AlgHom` version of `AdicCompletion.liftRingHom`.  -/
AdicCompletion.liftAlgHom : {S : Type u_5} →
  [inst : CommRing S] →
    (I : Ideal S) →
      {R : Type u_6} →
        {A : Type u_7} →
          [inst_1 : CommRing R] →
            [inst_2 : CommRing A] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R S] →
                  (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) →
                    (∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) →
                      A →ₐ[R] AdicCompletion I S
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.del.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_15) (fvarId_1 : Lean.FVarId)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_15),
  (Lean.Compiler.LCNF.CodeDecl.del fvarId h = Lean.Compiler.LCNF.CodeDecl.del fvarId_1 h_1) = (fvarId = fvarId_1)
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_apply_nonneg : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f : α → M} {a : α},
  (a ∈ s → 0 ≤ f a) → 0 ≤ s.indicator f a
-- Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Polynomial.cardPowDegree_apply : ∀ {Fq : Type u_1} [inst : Field Fq] [inst_1 : Fintype Fq] [inst_2 : DecidableEq Fq] (p : Polynomial Fq),
  Polynomial.cardPowDegree p = if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.completionFunctor_map : ∀ {X Y : UniformSpaceCat} (f : X ⟶ Y),
  UniformSpaceCat.completionFunctor.map f =
    CategoryTheory.ConcreteCategory.ofHom ⟨UniformSpace.Completion.map ⇑f.hom', ⋯⟩
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.empty_mem : ∀ {α : Type u_1} {C : Set (Set α)}, MeasureTheory.IsSetRing C → ∅ ∈ C
-- Mathlib.Algebra.Order.Group.Finset
Finset.sup_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [CanonicallyOrderedAdd M]
  [inst_3 : Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [inst_6 : OrderBot M],
  s.Nonempty → ∀ (f : ι → M) (a : M), s.sup f + a = s.sup fun i => f i + a
-- Aesop.Script.TacticState
_private.Aesop.Script.TacticState.0.Aesop.Script.TacticState.replaceWithArray : {α : Type} → [BEq α] → Array α → α → Array α → Option (Array α)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.leftZigzagIso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  (CategoryTheory.Bicategory.leftZigzagIso η ε).hom = CategoryTheory.Bicategory.leftZigzag η.hom ε.hom
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (↑(m.alter k f)).isEmpty = (((↑m).isEmpty || (↑m).size == 1 && m.contains k) && (f (m.get? k)).isNone)
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_insertEntry_of_key_beq_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)}
  (p : (a : α) × β a), (p.fst == a) = false → (p ∈ Std.Internal.List.insertEntry a b l ↔ p ∈ l)
-- Mathlib.Algebra.Group.Int.Even
Int.one_emod_two : 1 % 2 = 1
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
_private.Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite.0.step2 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E),
  IsClosed ↑A →
    ∀ [A.CoFG],
      Disjoint (↑u).ker A →
        (↑u).range = ⊤ →
          (Topology.IsStrictMap ⇑u ↔ Topology.IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed ↑(↑(u.domRestrict A)).range)