mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Attach
Array.attachWith_map_val : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {xs : Array α} (H : ∀ a ∈ xs, p a),
  Array.map (fun i => f ↑i) (xs.attachWith p H) = Array.map f xs
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.le_domRestrict : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f g : L.PartialEquiv M N) {A : L.Substructure M}, f.dom ≤ A → ∀ (hg : A ≤ g.dom), f ≤ g → f ≤ g.domRestrict hg
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_normalizer_iff'' : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {g : G},
  g ∈ AddSubgroup.normalizer ↑H ↔ ∀ (h : G), h ∈ H ↔ -g + h + g ∈ H
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.eq_normS : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.eq_normS_cert lhs rhs = true →
    Lean.Grind.CommRing.Expr.denoteS ctx lhs = Lean.Grind.CommRing.Expr.denoteS ctx rhs
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffOn.inter : ∀ {𝕜 : 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] {s t : Set M},
  UniqueMDiff[s] → IsOpen t → UniqueMDiff[s ∩ t]
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_iSup : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {ι : Sort u_7} (f : G →+ N)
  (s : ι → AddSubgroup G), AddSubgroup.map f (iSup s) = ⨆ i, AddSubgroup.map f (s i)
-- Init.Data.UInt.Bitwise
commandDeclare_bitwise_uint_theorems__ : Lean.ParserDescr
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balLeft.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (r : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r),
  (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α), r = RBTree.RBNode.node RBTree.RBColor.black a y b → False) →
    (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α) (c : RBTree.RBNode α),
        r = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c → False) →
      (match r with
        | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
        | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
        | r => h_3 r) =
        h_3 r
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.orderHom_injective : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {N : Type u_2}
  [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N] {f : M →+o N},
  Function.Injective ⇑f → Function.Injective ⇑(ArchimedeanClass.orderHom f)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.cast_rfl : ∀ {n : ℕ} (c : Composition n), c.cast ⋯ = c
-- Mathlib.Topology.Algebra.Group.Defs
Continuous.div' : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Div G]
  [ContinuousDiv G] {f g : X → G}, Continuous f → Continuous g → Continuous (f / g)
-- Mathlib.Data.Finset.Max
Finset.min'_mem : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.min' H ∈ s
-- Mathlib.RepresentationTheory.Coinduced
/-- If `φ : G →* H` and `A : Rep k G` then the `k`-submodule of functions `f : H → A`
such that for all `g : G`, `h : H`, `f (φ g * h) = A.ρ g (f h)`, is `k`-linearly equivalent
to the `G`-representation morphisms `k[H] ⟶ A`.  -/
Rep.coindVEquiv : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) →
              (A : Rep.{max u w, u, v} k G) → ↥(Representation.coindV φ A.ρ) ≃ₗ[k] Rep.res φ (Rep.leftRegular k H) ⟶ A
-- Mathlib.Algebra.Lie.Abelian
TrivialLieModule.instAddCommGroup : (R : Type u_1) → (L : Type u_2) → (M : Type u_3) → [AddCommGroup M] → AddCommGroup (TrivialLieModule R L M)
-- Init.Data.Array.Monadic
Array.forM_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] {as bs : Array α},
  as = bs → ∀ {f : α → m PUnit.{u_1 + 1}}, forM as f = forM bs f
-- Mathlib.Algebra.GroupWithZero.Conj
GroupWithZero.conj_pow₀ : ∀ {α : Type u_1} [inst : GroupWithZero α] {s : ℕ} {a d : α}, a ≠ 0 → (a⁻¹ * d * a) ^ s = a⁻¹ * d ^ s * a
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.instDecidableEq : DecidableEq Turing.PartrecToTM2.Λ'
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.awayι.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f f_deg hm).inv
      (AlgebraicGeometry.Proj.basicOpen 𝒜 f).ι
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.Hom.mk.injEq : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} (hom hom_1 : F X ⟶ F Y),
  ({ hom := hom } = { hom := hom_1 }) = (hom = hom_1)
-- Mathlib.Topology.Compactness.CountablyCompact
isCountablyCompact_iff_countablyCompactSpace : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E}, IsCountablyCompact A ↔ CountablyCompactSpace ↑A
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker.sizeOf_spec : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (η : Mathlib.Tactic.BicategoryLike.WhiskerRight)
  (f : Mathlib.Tactic.BicategoryLike.Atom₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker e η f) = 1 + sizeOf e + sizeOf η + sizeOf f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingular_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) {u : R},
  IsUnit u → (W'.Nonsingular (u • P) ↔ W'.Nonsingular P)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_zero_X_mul : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), (PowerSeries.coeff 0) (PowerSeries.X * φ) = 0
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.fixedBy_mul_eq_empty_iff : ∀ {M : Type u_3} [inst : Monoid M] [IsRightCancelMul M] {m : M}, MulAction.fixedBy M m = ∅ ↔ m ≠ 1
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_of_aemeasurable_trim : ∀ {β : Type u_3} [inst : MeasurableSpace β] {α : Type u_7} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) {f : α → β}, AEMeasurable f (μ.trim hm) → AEMeasurable f μ
-- Mathlib.RingTheory.DedekindDomain.PID
FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Submonoid R}
  [IsLocalization S A] (I : (FractionalIdeal S A)ˣ) {v : A},
  v ∈ ↑I⁻¹ → Submodule.comap (Algebra.linearMap R A) (↑↑I * (R ∙ v)) = ⊤ → (↑↑I).IsPrincipal
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Alias** of `intervalIntegral.integral_deriv_smul_comp'''`.

---

Change of variables, general form. If `f` is continuous on `[a, b]` and has
right-derivative `f'` in `(a, b)`, `g` is continuous on `f '' (a, b)` and integrable on
`f '' [a, b]`, and `f' x • (g ∘ f) x` is integrable on `[a, b]`,
then we can substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.

If the function `f` is monotone or antitone, see also `integral_deriv_smul_comp_of_deriv_nonneg`
and `integral_deriv_smul_comp_of_deriv_nonpos` dropping all assumptions on `g`.  -/
intervalIntegral.integral_comp_smul_deriv''' : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn g (f '' Set.Ioo (min a b) (max a b)) →
        MeasureTheory.IntegrableOn g (f '' Set.uIcc a b) MeasureTheory.volume →
          MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) (Set.uIcc a b) MeasureTheory.volume →
            ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The stabilizer of a point `a` as a submonoid of `M`.  -/
MulAction.stabilizerSubmonoid : (M : Type u_1) → {α : Type u_3} → [inst : Monoid M] → [MulAction M α] → α → Submonoid M
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_natCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocMod hp a (b + ↑m * p) = toIocMod hp a b
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.add.sizeOf_spec : ∀ (a b : Nat.Internal.Linear.Expr), sizeOf (a.add b) = 1 + sizeOf a + sizeOf b
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivWithinAt.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {f' g' : StrongDual ℂ E} {x : E}
  {s : Set E},
  HasFDerivWithinAt f f' s x →
    HasFDerivWithinAt g g' s x →
      f x ∈ Complex.slitPlane →
        HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x
-- Mathlib.Util.Superscript
/-- A mapping from superscripts to and from regular text.  -/
Mathlib.Tactic.Superscript.Mapping.superscript : Mathlib.Tactic.Superscript.Mapping
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imKₗ_apply : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R] (self : QuaternionAlgebra R c₁ c₂ c₃),
  (QuaternionAlgebra.imKₗ c₁ c₂ c₃) self = self.imK
-- Mathlib.Data.Set.Insert
Set.singleton_inter_eq_empty : ∀ {α : Type u_1} {s : Set α} {a : α}, {a} ∩ s = ∅ ↔ a ∉ s
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsGLB.neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G},
  IsGLB s a → IsLUB (-s) (-a)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.preservesCokernel_zero : ∀ {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]
  (X Y : C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair 0 0) G
-- Mathlib.Analysis.Normed.Group.Basic
dist_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], dist 0 = norm
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.archimedeanClassMk_neg_of_tendsto_atBot : ∀ {x : ℝ*}, Filter.Germ.Tendsto x Filter.atBot → ArchimedeanClass.mk x < 0
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_rpow_inv : ∀ {y : ℝ}, y ≠ 0 → ∀ (x : ENNReal), (x ^ y) ^ y⁻¹ = x
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_comp_commIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (g : E →L[𝕜] F),
  ContinuousLinearMap.rTensor G g ∘SL ↑↑(TensorProduct.commIsometry 𝕜 G E) =
    ↑↑(TensorProduct.commIsometry 𝕜 G F) ∘SL ContinuousLinearMap.lTensor G g
-- Mathlib.LinearAlgebra.Dual.Defs
Module.bijective_dual_eval : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsReflexive R M], Function.Bijective ⇑(Module.Dual.eval R M)
-- Mathlib.FieldTheory.AbelRuffini
solvableByRad_le : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {s : IntermediateField F E},
  (∀ (x : E) (n : ℕ), n ≠ 0 → x ^ n ∈ s → x ∈ s) → solvableByRad F E ≤ s
-- Mathlib.Computability.Primrec.List
Primrec.vector_toList : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec List.Vector.toList
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- If `P u` is `False` for any set `u` that has nonempty intersection both with `s` and `t`, then
`μ (s ∪ t) = μ s + μ t`, where `μ = inducedOuterMeasure m P0 m0`.

E.g., if `α` is an (e)metric space and `P u = diam u < r`, then this lemma implies that
`μ (s ∪ t) = μ s + μ t` on any two sets such that `r ≤ edist x y` for all `x ∈ s` and `y ∈ t`.  -/
MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} {s t : Set α},
  (∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → ¬P u) →
    (MeasureTheory.inducedOuterMeasure m P0 m0) (s ∪ t) =
      (MeasureTheory.inducedOuterMeasure m P0 m0) s + (MeasureTheory.inducedOuterMeasure m P0 m0) t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The `X`-coordinate of `(x₁, y₁) + (x₂, y₂)` for two nonsingular affine points `(x₁, y₁)` and
`(x₂, y₂)` on a Weierstrass curve `W`, where the line through them has a slope of `ℓ`.

This depends on `W`, and has argument order: `x₁`, `x₂`, `ℓ`.  -/
WeierstrassCurve.Affine.addX : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → R → R → R → R
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.toFun_eq_coe : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k), f.toFun = ⇑f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
          k ∈ List.map Sigma.fst l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).getKey k' h' = k
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_mk : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {f : A →ₐ[R] B}
  (h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → f.toRingHom x ∈ ℬ i), ⇑{ toAlgHom := f, map_mem := h } = ⇑f
-- Mathlib.RingTheory.FinitePresentation
RingHom.FinitePresentation.of_surjective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (f : A →+* B),
  Function.Surjective ⇑f → (RingHom.ker f).FG → f.FinitePresentation
-- Lean.Structure
_private.Lean.Structure.0.Lean.StructureState.mk : Lean.PersistentHashMap Lean.Name Lean.StructureInfo → Lean.StructureState✝
-- Mathlib.Algebra.Algebra.Operations
/-- Sub-`R`-modules of an `R`-module form an idempotent semiring.  -/
Submodule.instNonUnitalSemiring : {R : Type u} →
  [inst : Semiring R] →
    {A : Type v} →
      [inst_1 : Semiring A] → [inst_2 : Module R A] → [IsScalarTower R A A] → NonUnitalSemiring (Submodule R A)
-- Lean.Meta.Closure
Lean.Meta.Closure.pushToProcess : Lean.Meta.Closure.ToProcessElement → Lean.Meta.Closure.ClosureM Unit
-- Mathlib.RingTheory.Unramified.Pi
Algebra.FormallyUnramified.pi_iff : ∀ {R : Type u_1} {I : Type u_2} [Finite I] (f : I → Type u_3) [inst : CommRing R] [inst_1 : (i : I) → CommRing (f i)]
  [inst_2 : (i : I) → Algebra R (f i)],
  Algebra.FormallyUnramified R ((i : I) → f i) ↔ ∀ (i : I), Algebra.FormallyUnramified R (f i)
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.widePushout_exists_rep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {B : C}
  {α : Type v} {X : α → C} (f : (j : α) → B ⟶ X j) [inst_3 : CategoryTheory.Limits.HasWidePushout B X f]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.WidePushoutShape.wideSpan B X f)
      (CategoryTheory.forget C)]
  (x : CategoryTheory.ToType (CategoryTheory.Limits.widePushout B X f)),
  (∃ y, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePushout.head f)) y = x) ∨
    ∃ i y, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePushout.ι f i)) y = x
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (next' : α) → none = some next' → motive (some next'))
  (h_2 : none = none → motive none),
  (match hs : none with
    | some next' => h_1 next' hs
    | none => h_2 hs) =
    h_2 ⋯
-- Lean.Parser.Term
Lean.Parser.Term.letIdBinder : Lean.Parser.Parser
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Valued.v.Integers ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))
      ((t.truncGELTToLTGE a b).app X) =
    (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- A pseudometric space is proper if all closed balls are compact.  -/
ProperSpace : (α : Type u) → [PseudoMetricSpace α] → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlight.range : Lean.Lsp.DocumentHighlight → Lean.Lsp.Range
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.comp.sizeOf_spec : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.PartrecToTM2.Cont'),
  sizeOf (Turing.PartrecToTM2.Cont'.comp a a_1) = 1 + sizeOf a + sizeOf a_1
-- Aesop.Search.Expansion.Norm
Aesop.NormM.Context.ruleSet : Aesop.NormM.Context → Aesop.LocalRuleSet
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun_continuous : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], Continuous NumberField.mixedEmbedding.convexBodySumFun
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toNonUnitalSubalgebra_inj : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S U : Subalgebra R A},
  S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra ↔ S = U
-- Aesop.Options.Public
/-- (aesop) Only for use by Aesop developers. Enables the new stateful forward reasoning engine.
 -/
Aesop.aesop.dev.statefulForward : Lean.Option Bool
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₁.get k ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.ext'_iff : ∀ {X : SSet} {n : ℕ} {f g : X.Path (n + 1)}, f = g ↔ ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_union : ∀ {x y z : ZFSet.{u}}, z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- **Halmos' theorem: Haar measure is completion regular.** More precisely, any finite measure
set can be approximated from inside by a level set of a continuous function with compact
support.  -/
MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop],
  μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s =>
    MeasurableSet s ∧ μ s ≠ ⊤
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMany!_eq_foldl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β},
  ↑(t.insertMany! l) =
    List.foldl
      (fun acc x_1 =>
        match x_1 with
        | ⟨k, v⟩ => Std.DTreeMap.Internal.Impl.insert! k v acc)
      t l
-- Mathlib.Algebra.Order.Pi
Function.extend_nonpos : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Zero γ] [inst_1 : LE γ] {f : α → β} {g : α → γ} {e : β → γ},
  g ≤ 0 → e ≤ 0 → Function.extend f g e ≤ 0
-- Mathlib.Topology.MetricSpace.Defs
/-- Construct a metric space structure whose underlying topological space structure
(definitionally) agrees which a pre-existing topology which is compatible with a given distance
function.  -/
MetricSpace.ofDistTopology : {α : Type u} →
  [inst : TopologicalSpace α] →
    (dist : α → α → ℝ) →
      (∀ (x : α), dist x x = 0) →
        (∀ (x y : α), dist x y = dist y x) →
          (∀ (x y z : α), dist x z ≤ dist x y + dist y z) →
            (∀ (s : Set α), IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : α), dist x y < ε → y ∈ s) →
              (∀ (x y : α), dist x y = 0 → x = y) → MetricSpace α
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.eq_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) {x : β} {y : α},
  y = e.symm x ↔ e y = x
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {R : Type u_2} [inst_3 : Monoid R] [inst_4 : DistribMulAction R F]
  [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R), DifferentiableAt 𝕜 f x → deriv (c • f) x = c • deriv f x
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
IsCompl.prod_mul_prod : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Fintype ι] {s t : Finset ι},
  IsCompl s t → ∀ (f : ι → M), (∏ i ∈ s, f i) * ∏ i ∈ t, f i = ∏ i, f i
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom h)