mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Connected.CardComponents
IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → IsClosedMap f → ∀ [ConnectedSpace Y] {y : Y}, (f ⁻¹' {y}).Finite → Finite (ConnectedComponents X)
-- Mathlib.Probability.Process.Adapted
/-- The norm of a strongly progressive process is strongly progressive.  -/
MeasureTheory.IsStronglyProgressive.norm : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  [inst_1 : MeasurableSpace ι] {β : Type u_4} {u : ι → Ω → β} [inst_2 : SeminormedAddCommGroup β],
  MeasureTheory.IsStronglyProgressive f u → MeasureTheory.IsStronglyProgressive f fun t ω => ‖u t ω‖
-- Lean.Elab.Term.TermElabM
/-- Return true if mvarId is an auxiliary metavariable created for compiling `let rec` or it
is delayed assigned to one.  -/
Lean.Elab.Term.isLetRecAuxMVar : Lean.MVarId → Lean.Elab.TermElabM Bool
-- Mathlib.Topology.ContinuousOn
/-- If a function is continuous on two open sets, it is also continuous on their union.  -/
ContinuousOn.union_of_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s t : Set α} {f : α → β},
  ContinuousOn f s → ContinuousOn f t → IsOpen s → IsOpen t → ContinuousOn f (s ∪ t)
-- Mathlib.Data.Finset.Sups
Finset.forall_mem_diffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α} {p : α → Prop},
  (∀ c ∈ s.diffs t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a \ b)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.coeFn_toLp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] (f : SchwartzMap E F) (p : ENNReal)
  (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.coeFn_toLp._auto_1) [hμ : μ.HasTemperateGrowth],
  ↑↑(f.toLp p μ) =ᵐ[μ] ⇑f
-- Batteries.Data.List.Interleave
List.countP_interleave : ∀ {α : Type u_1} (l₁ l₂ : List α) (p : α → Bool), List.countP p (l₁.interleave l₂) = List.countP p l₁ + List.countP p l₂
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_subset_add_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₂_p : ∀ {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₁₃),
  CategoryTheory.CategoryStruct.comp h.p₁₂ h₁₂.p = h.p
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.max? = some km → t.contains km = true
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.bypass_eq_self_of_length_le_length_bypass`. -/
SimpleGraph.Walk.bypass_eq_self_of_length_le : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v),
  p.length ≤ p.bypass.length → p.bypass = p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.eq_empty_iff_forall_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t = ∅ ↔ ∀ (a : α), t.contains a = false
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas
Std.Tactic.BVDecide.BVLogicalExpr.unsat_of_bitblast : ∀ (expr : Std.Tactic.BVDecide.BVLogicalExpr), expr.bitblast.Unsat → expr.Unsat
-- Mathlib.InformationTheory.Hamming
Hamming.ofHamming_add : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Add (β i)] {x y : Hamming β},
  Hamming.ofHamming (x + y) = Hamming.ofHamming x + Hamming.ofHamming y
-- Mathlib.Algebra.Homology.CochainComplexPlus
/-- The functor on categories of bounded below cochain complexes that
is induced by a functor (which preserves zero morphisms).  -/
CategoryTheory.Functor.mapCochainComplexPlus : {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] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
              [F.PreservesZeroMorphisms] → CategoryTheory.Functor (CochainComplex.Plus C) (CochainComplex.Plus D)
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle** on a closed ball. Suppose that a function `f : E → F` from a
normed complex space to a strictly convex normed complex space has the following properties:

- it is continuous on a closed ball `Metric.closedBall z r`,
- it is complex differentiable on the corresponding open ball;
- the norm `‖f w‖` takes its maximum value on the open ball at its center.

Then `f` is a constant on the closed ball.  -/
Complex.eqOn_closedBall_of_isMaxOn_norm : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [StrictConvexSpace ℝ F] {f : E → F} {z : E} {r : ℝ},
  DiffContOnCl ℂ f (Metric.ball z r) →
    IsMaxOn (norm ∘ f) (Metric.ball z r) z → Set.EqOn f (Function.const E (f z)) (Metric.closedBall z r)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.ord_term_aux : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2), Profinite.NobelingProof.ord I (Profinite.NobelingProof.term I ho) = o
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.mem_supp_iff : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) (v : V), v ∈ C.supp ↔ G.connectedComponentMk v = C
-- Mathlib.Lean.Elab.Tactic.Meta
/-- Apply the given tactic code to `mvarId` in `MetaM`.

This is a variant of `Lean.Elab.runTactic` that forgets the final `Term.State`.
 -/
Lean.Elab.runTactic' : Lean.MVarId →
  Lean.Syntax → optParam Lean.Elab.Term.Context { } → optParam Lean.Elab.Term.State { } → Lean.MetaM (List Lean.MVarId)
-- Init.Data.Order.Lemmas
Std.Trichotomous.antisymm_not : ∀ {α : Sort u_1} {r : α → α → Prop} [i : Std.Trichotomous r], Std.Antisymm fun x1 x2 => ¬r x1 x2
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.sum_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} {p : ℕ} {ι : Type u_1} [inst_3 : Fintype ι]
  (α : ι → CategoryTheory.Abelian.Ext X Y p) {q : ℕ} (β : CategoryTheory.Abelian.Ext Y Z q) {n : ℕ} (h : p + q = n),
  (∑ i, α i).comp β h = ∑ i, (α i).comp β h
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgsResult.mk.injEq : ∀ (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray)
  (simpArgs : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)) (ctx_1 : Lean.Meta.Simp.Context)
  (simprocs_1 : Lean.Meta.Simp.SimprocsArray) (simpArgs_1 : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)),
  ({ ctx := ctx, simprocs := simprocs, simpArgs := simpArgs } =
      { ctx := ctx_1, simprocs := simprocs_1, simpArgs := simpArgs_1 }) =
    (ctx = ctx_1 ∧ simprocs = simprocs_1 ∧ simpArgs = simpArgs_1)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.subset_ndunion_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), t ⊆ s.ndunion t
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.divAll.eq_1 : ∀ (k k_1 : ℤ), Int.Internal.Linear.Poly.divAll k (Int.Internal.Linear.Poly.num k_1) = (k_1 % k == 0)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.instUnique : {V : Type u} → {G : SimpleGraph V} → [Unique V] → Unique G.ConnectedComponent
-- Mathlib.Data.Fin.Fin2
Fin2.ofFin_zero : ∀ (n : ℕ), Fin2.ofFin 0 = Fin2.fz
-- Init.SizeOf
String.ofByteArray.congr_simp : ∀ (toByteArray toByteArray_1 : ByteArray) (e_toByteArray : toByteArray = toByteArray_1)
  (isValidUTF8 : toByteArray.IsValidUTF8),
  { toByteArray := toByteArray, isValidUTF8 := isValidUTF8 } = { toByteArray := toByteArray_1, isValidUTF8 := ⋯ }
-- Mathlib.RingTheory.Filtration
/-- The `sup` of two `I.Filtration`s is an `I.Filtration`.  -/
Ideal.Filtration.instMax : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → Max (I.Filtration M)
-- Mathlib.Algebra.Group.Nat.Even
/-- If `m` and `n` are natural numbers, then the natural number `m^n` is even
if and only if `m` is even and `n` is positive.  -/
Nat.even_pow : ∀ {m n : ℕ}, Even (m ^ n) ↔ Even m ∧ n ≠ 0
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ico_pred_right_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a b : α},
  a < b → insert (Order.pred b) (Finset.Ico a (Order.pred b)) = Finset.Ico a b
-- Init.Data.Order.MinMaxOn
maxOn_eq_right_of_lt : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.Total fun x1 x2 => x1 ≤ x2]
  [Std.LawfulOrderLT β] {f : α → β} {x y : α}, f x < f y → maxOn f x y = y
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balance2.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (x_1 : α) →
        (x_2 : RBTree.RBNode α) →
          ((a : RBTree.RBNode α) →
              (x : α) →
                (b : RBTree.RBNode α) →
                  (y : α) →
                    (c : RBTree.RBNode α) →
                      (z : α) →
                        (d : RBTree.RBNode α) →
                          motive a x
                            (RBTree.RBNode.node RBTree.RBColor.red b y (RBTree.RBNode.node RBTree.RBColor.red c z d))) →
            ((a : RBTree.RBNode α) →
                (x : α) →
                  (b : RBTree.RBNode α) →
                    (y : α) →
                      (c : RBTree.RBNode α) →
                        (z : α) →
                          (d : RBTree.RBNode α) →
                            (∀ (c : RBTree.RBNode α) (z : α) (d_1 : RBTree.RBNode α),
                                d = RBTree.RBNode.node RBTree.RBColor.red c z d_1 → False) →
                              motive a x
                                (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b y c) z
                                  d)) →
              ((a : RBTree.RBNode α) →
                  (x : α) →
                    (b : RBTree.RBNode α) →
                      (∀ (b_1 : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α),
                          b =
                              RBTree.RBNode.node RBTree.RBColor.red b_1 y
                                (RBTree.RBNode.node RBTree.RBColor.red c z d) →
                            False) →
                        (∀ (b_1 : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α) (z : α) (d : RBTree.RBNode α),
                            b =
                                RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red b_1 y c) z
                                  d →
                              False) →
                          motive a x b) →
                motive x x_1 x_2
-- Lean.Elab.Tactic.Induction
/-- Returns the `inductionAlt` `ident <|> hole`  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getAltNameStx : Lean.Syntax → Lean.Syntax
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.toQ_inj : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [Lean.Grind.AddRightCancel α] {a b : α},
  Lean.Grind.IntModule.OfNatModule.toQ a = Lean.Grind.IntModule.OfNatModule.toQ b → a = b
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → α},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ μ →
    f ⁻¹' s =ᵐ[μ] s → Filter.limsup (fun n => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
-- Mathlib.Algebra.Group.Prod
AddHom.coprod_apply : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : AddCommSemigroup P]
  (f : M →ₙ+ P) (g : N →ₙ+ P) (p : M × N), (f.coprod g) p = f p.1 + g p.2
-- Mathlib.Computability.Ackermann
/-- If `f` is primitive recursive, there exists `m` such that `f n < ack m n` for all `n`.  -/
exists_lt_ack_of_nat_primrec : ∀ {f : ℕ → ℕ}, Nat.Primrec f → ∃ m, ∀ (n : ℕ), f n < ack m n
-- Init.Data.UInt.Basic
/-- Bitwise exclusive or for 32-bit unsigned integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.xor : UInt32 → UInt32 → UInt32
-- Mathlib.Order.Defs.LinearOrder
LinearOrder.toMin : {α : Type u_2} → [self : LinearOrder α] → Min α
-- Lean.Meta.ACLt
/-- An AC-compatible ordering.

Recall that an AC-compatible ordering if it is monotonic, well-founded, and total.
Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of
each expression in Lean 4. Even if we did, we would need to have a weight where implicit instance arguments are ignored.
So, we use a LPO-like term ordering.

Remark: this method is used to implement ordered rewriting. We ignore implicit instance
arguments to address an issue reported at issue #972.

Remark: the order is not really total on terms since
 - We instance implicit arguments.
 - We ignore metadata.
 - We ignore universe parameters at constants.
 -/
Lean.Meta.ACLt.main : Lean.Expr → Lean.Expr → optParam Lean.Meta.ACLt.ReduceMode Lean.Meta.ACLt.ReduceMode.none → Lean.MetaM Bool
-- Init.Data.Vector.Attach
Vector.countP_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {g : (a : α) → p a → β} {f : β → Bool} {xs : Vector α n}
  (H₁ : ∀ a ∈ xs, p a),
  Vector.countP f (Vector.pmap g xs H₁) =
    Vector.countP
      (fun x =>
        match x with
        | ⟨a, m⟩ => f (g a ⋯))
      xs.attach
-- Mathlib.Topology.Category.Compactum
Compactum.instConcreteCategoryHomA : CategoryTheory.ConcreteCategory Compactum fun x1 x2 => x1 ⟶ x2
-- Mathlib.Data.Nat.Prime.Defs
/-- **Alias** of the forward direction of `Nat.prime_iff`. -/
Nat.Prime.prime : ∀ {p : ℕ}, Nat.Prime p → Prime p
-- Init.Data.BEq
BEq.symm : ∀ {α : Type u_1} [inst : BEq α] [Std.Symm fun x1 x2 => (x1 == x2) = true] {a b : α}, (a == b) = true → (b == a) = true
-- Init.Data.List.Lemmas
List.eq_nil_of_length_eq_zero : ∀ {α : Type u_1} {l : List α}, l.length = 0 → l = []
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- The property of preserving cokernels expressed in terms of cokernel coforks.

This is a variant of `isColimitCoforkMapOfIsColimit` for equalizers,
which we can't use directly between `G.map 0 = 0` does not hold definitionally.
 -/
CategoryTheory.Limits.isColimitCoforkMapOfIsColimit' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [inst_4 : G.PreservesZeroMorphisms] →
                {X Y Z : C} →
                  {f : X ⟶ Y} →
                    {h : Y ⟶ Z} →
                      (w : CategoryTheory.CategoryStruct.comp f h = 0) →
                        [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] →
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ h w) →
                            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (G.map h) ⋯)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instInhabitedContext.default : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.instMonoFShortComplexObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), CategoryTheory.Mono (Φ.shortComplexObj X).f
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
`lift g m s = s⁻¹ • g m`.
 -/
LocalizedModule.lift_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (m : M) (s : ↥S),
  (LocalizedModule.lift S g h) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (g m)
-- Mathlib.Data.List.FinRange
List.nodup_ofFn : ∀ {α : Type u} {n : ℕ} {f : Fin n → α}, (List.ofFn f).Nodup ↔ Function.Injective f
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- The norm determinant of a linear map `f : U →ₗ[𝕜] V` is defined as the norm of the determinant of
the square matrix representing the linear map `U →ₗ[𝕜] f.range` over a pair of orthonormal basis of
equal dimensions.
(See `LinearMap.normDet_eq_norm_det_toMatrix_rangeRestrict` for using arbitrary orthonormal basis)

If such basis doesn't exist (e.g. the map is not injective), the norm determinant is zero.
(See `LinearMap.normDet_eq_zero_iff_ker_ne_bot`)
 -/
LinearMap.normDet : {𝕜 : Type u_1} →
  {U : Type u_2} →
    {V : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup U] →
          [inst_2 : InnerProductSpace 𝕜 U] →
            [FiniteDimensional 𝕜 U] →
              [inst_4 : NormedAddCommGroup V] → [inst_5 : InnerProductSpace 𝕜 V] → (U →ₗ[𝕜] V) → ℝ
-- Init.Coe
/-- `CoeDep α (x : α) β` is a typeclass for dependent coercions, that is, the type `β`
can depend on `x` (or rather, the value of `x` is available to typeclass search
so an instance that relates `β` to `x` is allowed).

Dependent coercions do not participate in the transitive chaining process of
regular coercions: they must exactly match the type mismatch on both sides.
 -/
CoeDep : (α : Sort u) → α → Sort v → Sort (max 1 v)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.smul_centroid_vsub_point_eq_smul_faceOppositeCentroid_vsub_point : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  (↑n + 1) • (s.centroid -ᵥ s.points i) = ↑n • (s.faceOppositeCentroid i -ᵥ s.points i)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionClientCapabilities.mk.sizeOf_spec : ∀ (dynamicRegistration? isPreferredSupport? disabledSupport? dataSupport? honorsChangeAnnotations? : Option Bool)
  (codeActionLiteralSupport? : Option Lean.Lsp.CodeActionLiteralSupport)
  (resolveSupport? : Option Lean.Lsp.ResolveSupport),
  sizeOf
      { dynamicRegistration? := dynamicRegistration?, isPreferredSupport? := isPreferredSupport?,
        disabledSupport? := disabledSupport?, dataSupport? := dataSupport?,
        honorsChangeAnnotations? := honorsChangeAnnotations?, codeActionLiteralSupport? := codeActionLiteralSupport?,
        resolveSupport? := resolveSupport? } =
    1 + sizeOf dynamicRegistration? + sizeOf isPreferredSupport? + sizeOf disabledSupport? + sizeOf dataSupport? +
          sizeOf honorsChangeAnnotations? +
        sizeOf codeActionLiteralSupport? +
      sizeOf resolveSupport?
-- Mathlib.Tactic.CrossRefAttribute
/-- The `stacksTag` attribute.
Use it as `@[kerodon TAG "Optional comment"]` or `@[stacks TAG "Optional comment"]`
depending on the database you are referencing.

The `TAG` is mandatory and should be a sequence of 4 digits or uppercase letters.

See the [Tags page](https://stacks.math.columbia.edu/tags) in the Stacks project or
[Tags page](https://kerodon.net/tag/) in the Kerodon project for more details.
 -/
Mathlib.CrossRef.stacksTag : Lean.ParserDescr
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.toZeroHom_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N), ⇑↑f = ⇑f
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω) μ
-- Mathlib.Topology.Constructions
IsOpen.isOpenEmbedding_subtypeVal : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → Topology.IsOpenEmbedding Subtype.val
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
AddOpposite.nndist_unop : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (x y : αᵃᵒᵖ),
  nndist (AddOpposite.unop x) (AddOpposite.unop y) = nndist x y
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.eq_1 : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ)
  (μ : MeasureTheory.Measure ℝ),
  intervalIntegral f a b μ = ∫ (x : ℝ) in Set.Ioc a b, f x ∂μ - ∫ (x : ℝ) in Set.Ioc b a, f x ∂μ
-- Mathlib.Tactic.FieldSimp
/-- Given a proof of the nonzeroness, strict positivity, etc. (as specified by the value of
`DenomCondition`) of a field-simp-normal-form expression `L` (a product of powers of atoms),
construct a corresponding proof for `((r, e), i) :: L`.  -/
Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' : {v : Lean.Level} →
  {M : Q(Type v)} →
    {iM : Q(CommGroupWithZero «$M»)} →
      ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
        {cond : Mathlib.Tactic.FieldSimp.DenomCondition q(inferInstance)} →
          {L : Mathlib.Tactic.FieldSimp.qNF M} →
            Mathlib.Tactic.FieldSimp.DenomCondition.proof L cond →
              (e : Q(«$M»)) →
                (r : ℤ) → (i : ℕ) → Lean.MetaM (Mathlib.Tactic.FieldSimp.DenomCondition.proof (((r, e), i) :: L) cond)
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.modify_bind_modifyGet : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (f : σ → σ) (g : σ → α × σ),
  (do
      modify f
      modifyGet g) =
    modifyGet (g ∘ f)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrp_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X Y : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H]
  (α : CategoryTheory.yonedaGrpObj G ⟶ CategoryTheory.yonedaGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G),
  (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
RootPairing.Base.root_sub_mem_iff_root_add_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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} [Finite ι] [P.IsCrystallographic] {b : P.Base} (i j k : ι),
  i ≠ j →
    i ∈ b.support →
      j ∈ b.support →
        k ≠ j →
          P.root k ≠ -P.root i →
            P.root k + P.root i - P.root j ∈ Set.range ⇑P.root →
              (P.root k - P.root j ∈ Set.range ⇑P.root ↔ P.root k + P.root i ∈ Set.range ⇑P.root)