mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
HasOuterApproxClosed.exAppr : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : HasOuterApproxClosed X] (F : Set X),
  IsClosed F →
    ∃ fseq,
      (∀ (n : ℕ) (x : X), (fseq n) x ≤ 1) ∧
        (∀ (n : ℕ), ∀ x ∈ F, 1 ≤ (fseq n) x) ∧
          Filter.Tendsto (fun n x => (fseq n) x) Filter.atTop (nhds (F.indicator fun x => 1))
-- Mathlib.Data.Complex.Basic
/-- A `Rectangle` is an axis-parallel rectangle with corners `z` and `w`.  -/
Complex.Rectangle : ℂ → ℂ → Set ℂ
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Iio_castLE : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a : Fin n),
  ∑ i < Fin.castLE h a, f i = ∑ i < a, f (Fin.castLE h i)
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.smallSchroder_zero : Nat.smallSchroder 0 = 1
-- Batteries.Data.PairingHeap
/-- `O(1)`. Is the heap empty?  -/
Batteries.PairingHeap.isEmpty : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → Bool
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges_biUnion_right : ∀ {ι : Type u_2} {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq α] (s : Finset α)
  (t : Finset ι) (f : ι → Finset α), G.interedges s (t.biUnion f) = t.biUnion fun b => G.interedges s (f b)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.cotangentEquivCotangentKer_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x : P.Cotangent), Algebra.Extension.cotangentEquivCotangentKer x = x.val
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_le_iff_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) {x : α}, Ideal.span {x} ≤ I ↔ x ∈ I
-- Mathlib.Algebra.RingQuot
RingQuot.mkAlgHom_def : ∀ (S : Type u_1) [inst : CommSemiring S] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra S A] (s : A → A → Prop),
  RingQuot.mkAlgHom S s =
    let __src := RingQuot.mkRingHom s;
    { toRingHom := __src, commutes' := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.HasProjectiveResolutions.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ (Z : C), CategoryTheory.HasProjectiveResolution Z) → CategoryTheory.HasProjectiveResolutions C
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PushoutCocone.op_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g), c.op.fst = c.inl.op
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_rightOp_of_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [CategoryTheory.Limits.HasLimit F], CategoryTheory.Limits.HasColimit F.rightOp
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_union : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α},
  m.IsCaratheodory s₁ → m.IsCaratheodory s₂ → m.IsCaratheodory (s₁ ∪ s₂)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_intCast_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (z : ℤ) (a : R),
  ⌈↑z + a⌉ = z + ⌈a⌉
-- Mathlib.Combinatorics.Graph.Basic
Graph.copy.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) {vertexSet : Set α} {edgeSet : Set β} {IsLink : β → α → α → Prop}
  (hvertexSet : G.vertexSet = vertexSet) (hedgeSet : G.edgeSet = edgeSet)
  (hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y),
  G.copy hvertexSet hedgeSet hIsLink =
    { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.length_toList_rco : ∀ {a b : ℕ}, (a...b).toList.length = b - a
-- Init.Internal.Order.Basic
Lean.Order.rel_f_of_iterates : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α},
  Lean.Order.monotone f → ∀ {x : α}, Lean.Order.iterates f x → Lean.Order.PartialOrder.rel x (f x)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inl_smul : ∀ {S : Type u_2} {R : Type u_3} (A : Type u_4) [inst : Zero A] [inst_1 : SMul S R] [inst_2 : SMulZeroClass S A] (s : S)
  (r : R), Unitization.inl (s • r) = s • Unitization.inl r
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t_fst_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f i))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g)) =
    CategoryTheory.Limits.pullback.snd
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
      (𝒰.f j)
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_int_mul : ∀ (z : ℂ) (n : ℤ), Complex.exp (↑n * z) = Complex.exp z ^ n
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.getMainModule : Lean.Elab.Tactic.TacticM Lean.Name
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, s.Nonempty → t.Nonempty → (s + t).Nonempty
-- Mathlib.ModelTheory.Quotients
FirstOrder.Language.Term.realize_quotient_mk' : ∀ {L : FirstOrder.Language} {M : Type u_1} (s : Setoid M) [ps : L.Prestructure s] {β : Type u_2} (t : L.Term β)
  (x : β → M), FirstOrder.Language.Term.realize (fun i => ⟦x i⟧) t = ⟦FirstOrder.Language.Term.realize x t⟧
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.of_separable_splitting_field : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {p : Polynomial F}
  [Polynomial.IsSplittingField F E p], p.Separable → IsGalois F E
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.spectrum_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : A) (x : ℝ),
  autoParam (ContinuousOn (fun x_1 => x_1 ^ x) (spectrum NNReal a)) CFC.spectrum_rpow._auto_1 →
    autoParam (0 ≤ a) CFC.spectrum_rpow._auto_3 → spectrum NNReal (a ^ x) = (fun x_1 => x_1 ^ x) '' spectrum NNReal a
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff_isIso_liftCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  S₁.f = 0 →
    ∀ (hg₁ : S₁.g = 0),
      S₂.f = 0 → (CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (S₂.liftCycles φ.τ₂ ⋯))
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- Polynomial evaluation commutes with `List.prod`
 -/
Polynomial.eval_list_prod : ∀ {R : Type u} [inst : CommSemiring R] (l : List (Polynomial R)) (x : R),
  Polynomial.eval x l.prod = (List.map (Polynomial.eval x) l).prod
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv : ∀ (R : Type u) [inst : CommRing R],
  (AlgebraicGeometry.StructureSheaf.globalSectionsIso R).inv =
    CommRingCat.ofHom
      ↑(RingEquiv.ofBijective (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op ⊤)))
            ⋯).symm
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The Mahler measure of a polynomial is at most the sup norm of the polynomial times the square
root of its degree plus one.  -/
Polynomial.mahlerMeasure_le_sqrt_natDegree_add_one_mul_supNorm : ∀ (p : Polynomial ℂ), p.mahlerMeasure ≤ √(↑p.natDegree + 1) * p.supNorm
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- Given functors `F₁` and `F₂` in `J ⥤ C`, where `C` is a category enriched in `V`,
this is the enriched hom functor from `F₁` to `F₂` in `J ⥤ V`.  -/
CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                (F₁ F₂ : CategoryTheory.Functor J C) →
                  [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] → CategoryTheory.Functor J V
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.negate.eq_1 : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), c.negate = List.map Std.Sat.Literal.negate c.clause
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instMulActionOfSMulCommClass : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {X : Type u_4} →
        {Y : Type u_5} →
          {σ : M → N} →
            [inst : SMul M X] →
              [inst_1 : SMul N Y] →
                [inst_2 : Monoid R] → [inst_3 : MulAction R Y] → [SMulCommClass N R Y] → MulAction R (X →ₑ[σ] Y)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.instNonUnitalSubsemiringClass : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], NonUnitalSubsemiringClass (NonUnitalSubsemiring R) R
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.Sign.instLawfulBEq_batteries : LawfulBEq Float.Model.UnpackedFloat.Sign
-- Mathlib.Order.Heyting.Basic
snd_sdiff : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiff α] [inst_1 : SDiff β] (a b : α × β), (b \ a).2 = b.2 \ a.2
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.mk : {S : Type u_2} →
  {M : Type u_3} →
    [inst : Add M] →
      [inst_1 : SMul S M] →
        (toAddCon : AddCon M) →
          (∀ (s : S) {x y : M}, toAddCon.toSetoid x y → toAddCon.toSetoid (s • x) (s • y)) → ModuleCon S M
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.isoMk_inv : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} {x : CommRing X} {x_1 : CommRing Y} {x_2 : Bialgebra R X}
  {x_3 : Bialgebra R Y} (e : X ≃ₐc[R] Y), (CommBialgCat.isoMk e).inv = CommBialgCat.ofHom ↑e.symm
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
/-- We choose `AddCommGrpCat.of (G × H)` as the product of `G` and `H` and
`AddCommGrpCat.of PUnit` as the terminal object.  -/
AddCommGrpCat.cartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory AddCommGrpCat
-- Mathlib.GroupTheory.Nilpotent
_private.Mathlib.GroupTheory.Nilpotent.0.Subgroup.upperCentralSeriesAux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Data.List.Nodup
List.Nodup.eq_of_head_mem_of_suffix : ∀ {α : Type u} {l₁ l₂ : List α}, l₁ <:+ l₂ → ∀ {hne : l₂ ≠ []}, l₂.head hne ∈ l₁ → l₂.Nodup → l₁ = l₂
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.map_add : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ.[σ] F)
  (x y : ↥f.domain), ↑f (x + y) = ↑f x + ↑f y
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
Real.convergent.eq_1 : ∀ (x : ℝ), x.convergent 0 = ↑⌊x⌋
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
/-- A simplicial set `S` is a Kan complex if it is fibrant, which means that
the projection `S ⟶ ⊤_ _` has the right lifting property with respect to horn inclusions.  -/
SSet.KanComplex : SSet → Prop
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.reindex_apply : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α),
  (Matrix.reindex eₘ eₙ) M = M.submatrix ⇑eₘ.symm ⇑eₙ.symm
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_associator_hom : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {L₀₁ : CategoryTheory.Functor A B} {R₁₀ : CategoryTheory.Functor B A}
  {L₁₂ : CategoryTheory.Functor B C} {R₂₁ : CategoryTheory.Functor C B} {L₂₃ : CategoryTheory.Functor C D}
  {R₃₂ : CategoryTheory.Functor D C} (adj₀₁ : L₀₁ ⊣ R₁₀) (adj₁₂ : L₁₂ ⊣ R₂₁) (adj₂₃ : L₂₃ ⊣ R₃₂),
  (CategoryTheory.conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃))
      (L₀₁.associator L₁₂ L₂₃).hom =
    (R₃₂.associator R₂₁ R₁₀).hom
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.any_keys : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → Bool}, m.keys.any p = m.any fun a x => p a
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_comp_map'_assoc : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g] (p : α → β)
  (q : (a : α) → f a ⟶ g (p a)) (a : α) {Z : C} (h : ∐ g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f a)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map' p q) h) =
    CategoryTheory.CategoryStruct.comp (q a)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g (p a)) h)
-- Init.Data.Option.Lemmas
/-- The `simp` normal form of `o.orElse f` is o.or (f ())`.  -/
Option.orElse_eq_or : ∀ {α : Type u_1} {o : Option α} {f : Unit → Option α}, o.orElse f = o.or (f ())
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.lift_comp_of : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] (f : α → M), ⇑(FreeMonoid.lift f) ∘ FreeMonoid.of = f
-- Mathlib.FieldTheory.Fixed
/-- The subfield of `F` fixed by the field endomorphism `m`.  -/
FixedBy.subfield : {M : Type u} → [inst : Monoid M] → (F : Type v) → [inst_1 : Field F] → [MulSemiringAction M F] → M → Subfield F
-- Mathlib.Algebra.Group.Action.Defs
/-- This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables.  -/
SMul.comp.smulCommClass' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul β α]
  [SMulCommClass β M α] (g : N → M), SMulCommClass β N α
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infinite_add : ∀ {x y : ℝ*}, ¬x.Infinite → ¬y.Infinite → ¬(x + y).Infinite
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instIsCancelAdd : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsCancelAdd (β i)],
  IsCancelAdd (Π₀ (i : ι), β i)
-- Mathlib.Analysis.Complex.Hadamard
/-- The transformation on ℂ that is used for `scale` maps the closed strip ``re ⁻¹' [l, u]``
to the closed strip ``re ⁻¹' [0, 1]``.  -/
Complex.HadamardThreeLines.scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip : ∀ {l u : ℝ},
  l < u →
    ∀ {z : ℂ},
      z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1 →
        ↑l + z * (↑u - ↑l) ∈ Complex.HadamardThreeLines.verticalClosedStrip l u
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.whiskerLeft_def : ∀ (R : Type u) [inst : CommRing R] (X x x_1 : BialgCat R) (f : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = BialgCat.ofHom (BialgHom.lTensor X.carrier f.toBialgHom')
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.smul : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] (r : MvPowerSeries τ S) {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a → PowerSeries.HasSubst (r • a)
-- Init.Data.Nat.Lemmas
Nat.pow_two : ∀ (a : ℕ), a ^ 2 = a * a
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instPow_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β], Lex.instPow_1 = inst
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult.mk : Lean.MetavarContext → Array Lean.Name → ℕ → Lean.Expr → Lean.MetavarContext.UnivMVarParamResult
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.bijective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Function.Bijective ⇑h
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSectionsOn.union : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → Set β} {s : Set α},
  HasOpenLowerSectionsOn f s → HasOpenLowerSectionsOn g s → HasOpenLowerSectionsOn (fun x => f x ∪ g x) s
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.eq_append_of_dropPrefix?_bool_eq_some : ∀ {p : Char → Bool} {s res : String.Slice},
  s.dropPrefix? p = some res → ∃ c, s.copy = String.singleton c ++ res.copy ∧ p c = true
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.mk_apply : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (d : X → X → R)
  (refl : ∀ (x : X), d x x = 0) (symm : ∀ (x y : X), d x y = d y x) (triangle : ∀ (x y z : X), d x z ≤ d x y + d y z)
  (x y : X), { toFun := d, refl' := refl, symm' := symm, triangle' := triangle } x y = d x y
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- **Alias** of the reverse direction of `contMDiffWithinAt_iff_contDiffWithinAt`. -/
ContDiffWithinAt.contMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {s : Set E} {x : E},
  ContDiffWithinAt 𝕜 n f s x → ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_elim_l : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, (P → Q) ∧ P ⊢ₛ Q
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.toLp_pi : ∀ {Ω : Type u_1} {ι : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : ι → Type u_5}
  [inst : (i : ι) → NormedAddCommGroup (E i)] [inst_1 : (i : ι) → NormedSpace ℝ (E i)]
  [inst_2 : (i : ι) → MeasurableSpace (E i)] [∀ (i : ι), BorelSpace (E i)] {X : (i : ι) → Ω → E i}
  [∀ (i : ι), SecondCountableTopology (E i)] [Finite ι] (p : ENNReal) [Fact (1 ≤ p)],
  ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P →
    ProbabilityTheory.HasGaussianLaw (fun ω => WithLp.toLp p fun x => X x ω) P
-- Mathlib.Analysis.InnerProductSpace.Continuous
continuous_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  Continuous fun p => inner 𝕜 p.1 p.2
-- Mathlib.CategoryTheory.Galois.Basic
/-- An object that is neither initial or connected has a non-trivial subobject.  -/
CategoryTheory.PreGaloisCategory.has_non_trivial_subobject_of_not_isConnected_of_not_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (X : C),
  ¬CategoryTheory.PreGaloisCategory.IsConnected X →
    (∀ (a : CategoryTheory.Limits.IsInitial X), False) →
      ∃ Y v, (∀ (a : CategoryTheory.Limits.IsInitial Y), False) ∧ CategoryTheory.Mono v ∧ ¬CategoryTheory.IsIso v
-- Init.Data.String.Lemmas.Basic
String.Pos.nextn_add_one : ∀ {n : ℕ} {s : String} {p : s.Pos}, p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
/-- The condition on a morphism `K.restriction e ⟶ L` which allows to
extend it as a morphism `K ⟶ L.extend e`, see `Embedding.homEquiv`.  -/
ComplexShape.Embedding.HasLift : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          {C : Type u_3} →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                {K : HomologicalComplex C c'} →
                  {L : HomologicalComplex C c} → [inst_2 : e.IsRelIff] → (K.restriction e ⟶ L) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.mk : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                  (left : ψ.left ⟶ ψ'.left) →
                                    (right : ψ.right ⟶ ψ'.right) →
                                      (base : ψ.base ⟶ ψ'.base) →
                                        autoParam
                                            (CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
                                                (CategoryTheory.Functor.whiskerRight left F') =
                                              CategoryTheory.CategoryStruct.comp (F.whiskerLeft base)
                                                (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
                                            CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence._autoParam →
                                          autoParam
                                              (CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
                                                  (CategoryTheory.Functor.whiskerRight right G') =
                                                CategoryTheory.CategoryStruct.comp (G.whiskerLeft base)
                                                  (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
                                              CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence._autoParam →
                                            CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ'