mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_comp_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β) {f : β → γ},
  Measurable f → ∀ {g : γ → δ}, Measurable g → κ.map (g ∘ f) = (κ.map f).map g
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instToStringOffset : ToString Std.Time.Minute.Offset
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.zero_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (f : α →ₙ+* β),
  NonUnitalRingHom.comp 0 f = 0
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opEquivalence_inverse : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.opEquivalence V c).inverse = HomologicalComplex.opInverse V c
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.vadd_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (X : D),
  CategoryTheory.AddModObj.vadd = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.aestronglyMeasurable : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → MeasureTheory.AEStronglyMeasurable X μ
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.perm_map_congr_left : ∀ {α : Type u} {β : Type v} {l l' : List α} {f : α → β} {l₂ : List β},
  l.Perm l' → ((List.map f l).Perm l₂ ↔ (List.map f l').Perm l₂)
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
/-- In a category with binary biproducts, the morphisms form a commutative monoid.  -/
CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] → (X Y : C) → AddCommMonoid (X ⟶ Y)
-- Mathlib.Topology.Metrizable.Basic
/-- A uniform space with countably generated `𝓤 X` is pseudometrizable.  -/
UniformSpace.pseudoMetrizableSpace : ∀ {X : Type u_5} [u : UniformSpace X] [hu : (uniformity X).IsCountablyGenerated],
  TopologicalSpace.PseudoMetrizableSpace X
-- Mathlib.Order.Monotone.Monovary
monovary_toDual_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Monovary f (⇑OrderDual.toDual ∘ g) ↔ Antivary f g
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabDo : Lean.PrettyPrinter.Delaborator.Delab
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.mk.injEq : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] (toArray : Array α) (toHashSet : Std.HashSet α)
  (toArray_1 : Array α) (toHashSet_1 : Std.HashSet α),
  ({ toArray := toArray, toHashSet := toHashSet } = { toArray := toArray_1, toHashSet := toHashSet_1 }) =
    (toArray = toArray_1 ∧ toHashSet = toHashSet_1)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_zsmul : ∀ (n : ℤ) (r : ℝ), ↑(n • r) = n • ↑r
-- Mathlib.RingTheory.FiniteType
RingHom.finiteType_algebraMap : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  (algebraMap A B).FiniteType ↔ Algebra.FiniteType A B
-- Mathlib.Algebra.Field.Defs
Field.toDiv : {K : Type u} → [self : Field K] → Div K
-- Mathlib.Algebra.AlgebraicCard
Algebraic.aleph0_le_cardinalMk_of_charZero : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [CharZero A],
  Cardinal.aleph0 ≤ Cardinal.mk { x // IsAlgebraic R x }
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.multisetSum_map_zero : ∀ {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Multiset α}, (∀ x ∈ s, f x ≡ 0 [ZMOD n]) → (Multiset.map f s).sum ≡ 0 [ZMOD n]
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.setCurr.match_1.eq_1 : ∀ (motive : String.Legacy.Iterator → Char → Sort u_1) (s : String) (i : String.Pos.Raw) (c : Char)
  (h_1 : (s : String) → (i : String.Pos.Raw) → (c : Char) → motive { s := s, i := i } c),
  (match { s := s, i := i }, c with
    | { s := s, i := i }, c => h_1 s i c) =
    h_1 s i c
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmaKey.mk.injEq : ∀ (type : Lean.Expr) (isPrivate defeq : Bool) (type_1 : Lean.Expr) (isPrivate_1 defeq_1 : Bool),
  ({ type := type, isPrivate := isPrivate, defeq := defeq } =
      { type := type_1, isPrivate := isPrivate_1, defeq := defeq_1 }) =
    (type = type_1 ∧ isPrivate = isPrivate_1 ∧ defeq = defeq_1)
-- Mathlib.Order.Heyting.Basic
le_compl_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a : α}, a ≤ aᶜ ↔ a = ⊥
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.none : Aesop.IndexMatchLocation
-- Lean.Declaration
/-- An inductive type is called reflexive if it has at least one constructor that takes as an argument a function returning the
same type we are defining.
Consider the type:
```
inductive WideTree where
| branch: (Nat -> WideTree) -> WideTree
| leaf: WideTree
```
this is reflexive due to the presence of the `branch : (Nat -> WideTree) -> WideTree` constructor.

See also: 'Inductive Definitions in the system Coq Rules and Properties' by Christine Paulin-Mohring
Section 2.2, Definition 3
 -/
Lean.InductiveVal.isReflexive : Lean.InductiveVal → Bool
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.hasBasis_nhds_of_ne_zero : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {x : Γ₀},
  x ≠ 0 → (nhds x).HasBasis (fun x => True) fun x_1 => {x}
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The category of affine schemes is equivalent to the category of commutative rings.  -/
AlgebraicGeometry.AffineScheme.equivCommRingCat : AlgebraicGeometry.AffineScheme ≌ CommRingCatᵒᵖ
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_snd : ∀ {𝕜 : 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] {p : E × F},
  HasFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.toSubtype.match_1.eq_2 : ∀
  (motive :
    (x : ℕ) →
      (x_1 : TypeVec.{u_1} x) →
        (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) →
          (x_3 : Fin2 x) → { x_4 // TypeVec.ofRepeat (x_2 x_3 x_4) } → Sort u_2)
  (n : ℕ) (x : TypeVec.{u_1} n.succ) (x_1 : x.Arrow (TypeVec.repeat n.succ Prop))
  (x_2 : { x // TypeVec.ofRepeat (x_1 Fin2.fz x) })
  (h_1 :
    (n : ℕ) →
      (x : TypeVec.{u_1} n.succ) →
        (p : x.Arrow (TypeVec.repeat n.succ Prop)) →
          (i : Fin2 n) → (x_3 : { x // TypeVec.ofRepeat (p i.fs x) }) → motive n.succ x p i.fs x_3)
  (h_2 :
    (n : ℕ) →
      (x : TypeVec.{u_1} n.succ) →
        (x_3 : x.Arrow (TypeVec.repeat n.succ Prop)) →
          (x_4 : { x // TypeVec.ofRepeat (x_3 Fin2.fz x) }) → motive n.succ x x_3 Fin2.fz x_4),
  (match n.succ, x, x_1, Fin2.fz, x_2 with
    | n.succ, x, p, i.fs, x_3 => h_1 n x p i x_3
    | n.succ, x, x_3, Fin2.fz, x_4 => h_2 n x x_3 x_4) =
    h_2 n x x_1 x_2
-- Mathlib.Dynamics.Transitive
/-- An action of an additive monoid `M` on a topological space `α` is called
*topologically transitive* if for any pair of nonempty open sets `U` and `V` in `α` there exists an
`m : M` such that `(m +ᵥ U) ∩ V` is nonempty.  -/
AddAction.IsTopologicallyTransitive : (M : Type u_1) → (α : Type u_2) → [inst : AddMonoid M] → [TopologicalSpace α] → [AddAction M α] → Prop
-- Batteries.Data.UnionFind.Basic
/-- Empty union-find structure  -/
Batteries.UnionFind.empty : Batteries.UnionFind
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x y : A` and Localization maps `F : A →+ B, G : A →+ C` away from `x` and `x + y`
respectively, the homomorphism induced from `B` to `C`.  -/
AddSubmonoid.LocalizationMap.awayToAwayRight : {A : Type u_4} →
  [inst : AddCommMonoid A] →
    (x : A) →
      {B : Type u_5} →
        [inst_1 : AddCommMonoid B] →
          AddSubmonoid.LocalizationMap.AwayMap x B →
            {C : Type u_6} →
              [inst_2 : AddCommMonoid C] → (y : A) → AddSubmonoid.LocalizationMap.AwayMap (x + y) C → B →+ C
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- See `Finset.Nonempty.card_nsmul_mono` for a version that works for zero scalars.  -/
Finset.card_nsmul_mono : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCancelMonoid α] {s : Finset α} {m n : ℕ},
  m ≠ 0 → m ≤ n → (m • s).card ≤ (n • s).card
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.toLinearMap_injective : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂}, Function.Injective LinearMap.BilinForm.Isometry.toLinearMap
-- Init.Omega.Int
Lean.Omega.Int.add_congr : ∀ {a b c d : ℤ}, a = b → c = d → a + c = b + d
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.leadingCoeff_sub : ∀ {R : Type u_3} [inst : AddGroup R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  x.orderTop < y.orderTop → (x - y).leadingCoeff = x.leadingCoeff
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- Riemann-Lebesgue Lemma for continuous and compactly-supported functions: the integral
`∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v` tends to 0 w.r.t. `cocompact V`. Note that this is primarily
of interest as a preparatory step for the more general result
`tendsto_integral_exp_inner_smul_cocompact` in which `f` can be arbitrary.  -/
tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support : ∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : V → E}
  [inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] [inst_5 : InnerProductSpace ℝ V]
  [inst_6 : FiniteDimensional ℝ V],
  Continuous f →
    HasCompactSupport f →
      Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v) (Filter.cocompact V) (nhds 0)
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsMulTorsionFree.pow_right_inj : ∀ {M : Type u_2} [inst : CancelMonoid M] [IsMulTorsionFree M] {x : M}, x ≠ 1 → ∀ {n m : ℕ}, x ^ n = x ^ m ↔ n = m
-- Batteries.Data.Fin.Coding
/-- Decode `(i : Fin n) → Fin (f i)` from `Fin (Fin.prod f)`.  -/
Fin.decodePi : {n : ℕ} → (f : Fin n → ℕ) → Fin (Fin.prod f) → (i : Fin n) → Fin (f i)
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.sub_eq_eval₁ : ∀ {R : Type u_2} {M : Type u_3} [inst : SMul R M] [inst_1 : AddGroup M] (a₁ : R × M) {a₂ : R × M}
  {l₁ l₂ l : Mathlib.Tactic.Module.NF R M},
  l₁.eval - (a₂ ::ᵣ l₂).eval = l.eval → (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
-- Batteries.Data.DList.Basic
/-- `O(1)` (`apply` is `O(1)`). Prepend `a` on a `DList α`.  -/
Batteries.DList.cons : {α : Type u} → α → Batteries.DList α → Batteries.DList α
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_add : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f g : Π₀ (i : ι), β i), DFinsupp.filter p (f + g) = DFinsupp.filter p f + DFinsupp.filter p g
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- A symmetric projection is a symmetric idempotent.  -/
LinearMap.IsSymmetricProjection : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →ₗ[𝕜] E) → Prop
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.minView!.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' => h_2 size k' v' l' r') =
    h_1 ()
-- Mathlib.LinearAlgebra.Matrix.MvPolynomial
Matrix.mvPolynomialX_apply : ∀ (m : Type u_1) (n : Type u_2) (R : Type u_3) [inst : CommSemiring R] (i : m) (j : n),
  Matrix.mvPolynomialX m n R i j = MvPolynomial.X (i, j)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.pruneFinishedWaiters : {m : Type → Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.AtomicT Std.Http.Body.Channel.State✝ m Unit
-- Mathlib.Analysis.Normed.Group.Ultra
/-- All triangles are isosceles in an ultrametric normed additive group.  -/
IsUltrametricDist.nnnorm_add_eq_max_of_nnnorm_ne_nnnorm : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] {x y : S}, ‖x‖₊ ≠ ‖y‖₊ → ‖x + y‖₊ = max ‖x‖₊ ‖y‖₊
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank_le_card_width : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] [inst_2 : Fintype n]
  (A : Matrix m n R), A.cRank ≤ ↑(Fintype.card n)
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.sequenceΨ.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X X_1 : CategoryTheory.Abelian.SpectralObject C ι),
  X = X_1 →
    ∀ {i j k l : ι} (f₁ f₁_1 : i ⟶ j) (e_f₁ : f₁ = f₁_1) (f₂ f₂_1 : j ⟶ k) (e_f₂ : f₂ = f₂_1) (f₃ f₃_1 : k ⟶ l)
      (e_f₃ : f₃ = f₃_1) (f₁₂ f₁₂_1 : i ⟶ k) (e_f₁₂ : f₁₂ = f₁₂_1)
      (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ f₂₃_1 : j ⟶ l) (e_f₂₃ : f₂₃ = f₂₃_1)
      (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1) (n₁ n₁_1 : ℤ)
      (e_n₁ : n₁ = n₁_1) (hn₁ : n₀ + 1 = n₁),
      X.sequenceΨ f₁ f₂ f₃ f₁₂ h₁₂ f₂₃ h₂₃ n₀ n₁ hn₁ = X_1.sequenceΨ f₁_1 f₂_1 f₃_1 f₁₂_1 ⋯ f₂₃_1 ⋯ n₀_1 n₁_1 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.copy_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I)
  (hm : autoParam (m = F.m) CategoryTheory.Limits.MonoFactorisation.copy._auto_1)
  (he : autoParam (e = F.e) CategoryTheory.Limits.MonoFactorisation.copy._auto_3), (F.copy m e hm he).I = F.I
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpOptions.mk : Lean.Lsp.WorkDoneProgressOptions → Option (Array String) → Option (Array String) → Lean.Lsp.SignatureHelpOptions
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.lift_unique : ∀ (R : Type u₁) {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u₃}
  [inst_3 : Ring A] [inst_4 : Algebra R A] (f : L →ₗ⁅R⁆ A) (g : UniversalEnvelopingAlgebra R L →ₐ[R] A),
  ⇑g ∘ ⇑(UniversalEnvelopingAlgebra.ι R) = ⇑f ↔ g = (UniversalEnvelopingAlgebra.lift R) f
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.mk.inj : ∀ {α : Type u} {β : Type v} {inst : PseudoEMetricSpace α} {inst_1 : PseudoEMetricSpace β} {toEquiv : α ≃ β}
  {isometry_toFun : Isometry toEquiv.toFun} {toEquiv_1 : α ≃ β} {isometry_toFun_1 : Isometry toEquiv_1.toFun},
  { toEquiv := toEquiv, isometry_toFun := isometry_toFun } =
      { toEquiv := toEquiv_1, isometry_toFun := isometry_toFun_1 } →
    toEquiv = toEquiv_1
-- Init.Grind.Interactive
/-- `finish` tries to close the current goal using `grind`'s default strategy  -/
Lean.Parser.Tactic.Grind.finish : Lean.ParserDescr
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.toDigitsCore.eq_def : ∀ (base x x_1 : ℕ) (x_2 : List Char),
  base.toDigitsCore x x_1 x_2 =
    match x, x_1, x_2 with
    | 0, x, ds => ds
    | fuel.succ, n, ds =>
      have d := (n % base).digitChar;
      have n' := n / base;
      if n' = 0 then d :: ds else base.toDigitsCore fuel n' (d :: ds)
-- Mathlib.Tactic.DepRewrite
/-- Given `e`, return `e'` where `e'` has had
- the occurrences of `p` in `ctx.cfg.occs` replaced by `x`; and
- subterms cast as appropriate in order to make `e'` type-correct.

If `et?` is not `none`, the output is guaranteed to have type (defeq to) `et?`.

We do _not_ assume that `e` is well-typed.
We use this when processing binders:
to traverse `∀ (x : α), β`,
we obtain `α' ← visit α`,
add `x : α'` to the local context
and continue traversing `β`.
Although `x : α' ⊢ β` may not hold,
the output `β'` should have `x : α' ⊢ β'` (otherwise we have a bug).

To achieve this, we maintain the invariant
that all entries in the local context that we have introduced
can be translated back to their original (pre-`visit`) types
using the motive computed by `castBack?.motive`.
(But we have not attempted to prove this.)  -/
Mathlib.Tactic.DepRewrite.visitAndCast : Lean.Expr → Option Lean.Expr → Mathlib.Tactic.DepRewrite.M Lean.Expr
-- Mathlib.NumberTheory.WellApproximable
approxOrderOf.image_pow_subset_of_coprime : ∀ {A : Type u_1} [inst : SeminormedCommGroup A] {m n : ℕ} (δ : ℝ),
  0 < m → n.Coprime m → (fun y => y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (↑m * δ)
-- Mathlib.Data.Finset.Sups
Finset.infs_union_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t₁ t₂ : Finset α},
  s ⊼ (t₁ ∪ t₂) = s ⊼ t₁ ∪ s ⊼ t₂
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
TensorProduct.eq_of_fg_of_subtype_eq : ∀ {R : Type u} {M : Type u_1} {N : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Submodule R M},
  P.FG →
    ∀ {t t' : TensorProduct R (↥P) N},
      (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P.subtype) t' →
        ∃ Q,
          ∃ (hPQ : P ≤ Q),
            Q.FG ∧
              (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_bmod_of_dvd : ∀ {a : ℤ} {n m : ℕ}, n ∣ m → (a.bmod m).bmod n = a.bmod n
-- Mathlib.Tactic.Linter.PPRoundtrip
/-- `polishPP s` takes as input a `String` `s`, assuming that it is the output of
pretty-printing a lean command.
The main intent is to convert `s` to a reasonable candidate for a desirable source code format.
The function first replaces consecutive whitespace sequences into a single space (` `), in an
attempt to side-step line-break differences.
After that, it applies some pre-emptive changes:
* doc-module beginnings tend to have some whitespace following them, so we add a space back in;
* name quotations such as ``` ``Nat``` get pretty-printed as ``` `` Nat```, so we remove a space
  after double back-ticks, but take care of adding one more for triple (or more) back-ticks;
* `notation3` is not followed by a pretty-printer space, so we add it here (https://github.com/leanprover-community/mathlib4/pull/15515).
 -/
_private.Mathlib.Tactic.Linter.PPRoundtrip.0.Mathlib.Linter.polishPP : String → String
-- Mathlib.Logic.Basic
lawful_beq_subsingleton : ∀ {α : Type u_1} (inst1 inst2 : BEq α) [LawfulBEq α] [LawfulBEq α], inst1 = inst2
-- Mathlib.Data.TypeVec
TypeVec.lastFun_toSubtype : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)),
  TypeVec.lastFun (TypeVec.toSubtype p) = id
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instPowNat : Pow Complex.UnitClosedDisc ℕ
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.antitone_iff_Icc : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
  [inst_2 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddCommGroup H] [inst_6 : PartialOrder H]
  [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F},
  0 < a → ∀ (l : G), Antitone ⇑f ↔ AntitoneOn (⇑f) (Set.Icc l (l + a))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insert k v).size = if t.contains k = true then t.size else t.size + 1
-- Batteries.Data.String.Lemmas
String.next_of_valid' : ∀ (cs cs' : List Char),
  String.Pos.Raw.next (String.ofList (cs ++ cs')) { byteIdx := String.utf8Len cs } =
    { byteIdx := String.utf8Len cs + (cs'.headD default).utf8Size }
-- Mathlib.Combinatorics.Enumerative.Composition
List.sum_take_map_length_splitWrtComposition : ∀ {α : Type u_1} (l : List α) (c : Composition l.length) (i : ℕ),
  (List.take i (List.map List.length (l.splitWrtComposition c))).sum = c.sizeUpTo i
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- If a product is anisotropic then its components must be. The converse is not true.  -/
QuadraticMap.anisotropic_of_prod : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P},
  (Q₁.prod Q₂).Anisotropic → Q₁.Anisotropic ∧ Q₂.Anisotropic
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.one_apply_ne : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R] {x : ℕ}, x ≠ 1 → 1 x = 0
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- With the optimal candidate, construct a premetric space structure on `X ⊕ Y`, on which the
predistance is given by the candidate. Then, we will identify points at `0` predistance
to obtain a genuine metric space.  -/
GromovHausdorff.premetricOptimalGHDist : (X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [CompactSpace X] →
        [Nonempty X] → [inst : MetricSpace Y] → [CompactSpace Y] → [Nonempty Y] → PseudoMetricSpace (X ⊕ Y)
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The cells making up a `YoungDiagram` from a list of row lengths  -/
YoungDiagram.cellsOfRowLens : List ℕ → Finset (ℕ × ℕ)
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.DTreeMap.Raw.minKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → α
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- An induction principle for closure membership. If `p` holds for `1` and all elements of `s`, and
is preserved under multiplication, then `p` holds for all elements of the closure of `s`.  -/
Submonoid.closure_induction : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {motive : (x : M) → x ∈ Submonoid.closure s → Prop},
  (∀ (x : M) (h : x ∈ s), motive x ⋯) →
    motive 1 ⋯ →
      (∀ (x y : M) (hx : x ∈ Submonoid.closure s) (hy : y ∈ Submonoid.closure s),
          motive x hx → motive y hy → motive (x * y) ⋯) →
        ∀ {x : M} (hx : x ∈ Submonoid.closure s), motive x hx
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Skips `numParams` binders, and execute `x varNames` where `varNames` contains the new binder names.
The `hNames` array is used for the last params.
Helper for `delabAppMatch`.
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.skippingBinders : {α : Type} →
  ℕ →
    Array Lean.Name →
      (Array Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM α) → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.toSubmonoid : {G : Type u_1} → [inst : CommGroup G] → GroupCone G → Submonoid G
-- Mathlib.Algebra.Group.Defs
inv_one : ∀ {G : Type u_1} [inst : InvOneClass G], 1⁻¹ = 1
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (f' : α → β) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'