mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.RelIso.Basic
RelEmbedding.mk.injEq : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (toEmbedding : α ↪ β)
  (map_rel_iff' : ∀ {a b : α}, s (toEmbedding a) (toEmbedding b) ↔ r a b) (toEmbedding_1 : α ↪ β)
  (map_rel_iff'_1 : ∀ {a b : α}, s (toEmbedding_1 a) (toEmbedding_1 b) ↔ r a b),
  ({ toEmbedding := toEmbedding, map_rel_iff' := map_rel_iff' } =
      { toEmbedding := toEmbedding_1, map_rel_iff' := map_rel_iff'_1 }) =
    (toEmbedding = toEmbedding_1)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_inv_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.mop =
    (CategoryTheory.MonoidalCategoryStruct.associator { unmop := Z } { unmop := Y } { unmop := X }).hom
-- Init.Data.SInt.Basic
/-- Arithmetic right shift for word-sized signed integers. Usually accessed via the `<<<` operator.

The high bits are filled with the value of
the most significant bit.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.shiftRight : ISize → ISize → ISize
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The Ore localization of a monoid and a submonoid fulfilling the Ore condition.  -/
OreLocalization : {R : Type u_1} →
  [inst : Monoid R] →
    (S : Submonoid R) → [OreLocalization.OreSet S] → (X : Type u_2) → [MulAction R X] → Type (max u_1 u_2)
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- In a space with an inner regular measure, the everywhere positive subset of a measurable set
is itself everywhere positive. This is not obvious as `μ.everywherePosSubset s` is defined as
the points whose neighborhoods intersect `s` along positive measure subsets, but this does not
say they also intersect `μ.everywherePosSubset s` along positive measure subsets.  -/
MeasureTheory.Measure.isEverywherePos_everywherePosSubset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [OpensMeasurableSpace α] [μ.InnerRegular], MeasurableSet s → μ.IsEverywherePos (μ.everywherePosSubset s)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.left_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C),
  CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.ε.app (self.obj X)) =
    CategoryTheory.CategoryStruct.id (self.obj X)
-- Mathlib.Data.PFun
PFun.coe_id : ∀ (α : Type u_7), ↑id = PFun.id α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
ContinuousAt.arccos : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {x : X},
  ContinuousAt f x → ContinuousAt (fun x => Real.arccos (f x)) x
-- Mathlib.Algebra.Algebra.Subalgebra.Pi
/-- The product of subalgebras as a subalgebra.  -/
Subalgebra.pi : {ι : Type u_1} →
  {R : Type u_2} →
    {S : ι → Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (S i)] →
          [inst_2 : (i : ι) → Algebra R (S i)] → Set ι → ((i : ι) → Subalgebra R (S i)) → Subalgebra R ((i : ι) → S i)
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_lt : ∀ (x : Int64), x.toNatClampNeg < 2 ^ 63
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleSets.mk.inj : ∀ {ruleSets ruleSets_1 : Array Aesop.RuleSetName},
  { ruleSets := ruleSets } = { ruleSets := ruleSets_1 } → ruleSets = ruleSets_1
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_inter_distrib_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)
-- Lean.Expr
/-- Return `Unit -> type`. Do not confuse with `Thunk type`  -/
Lean.mkSimpleThunkType : Lean.Expr → Lean.Expr
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_ge_a_pow : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), a ^ n ≤ Pell.xn a1 n
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : Mul α],
  OrderMonoidIso.instInhabited α = { default := OrderMonoidIso.refl α }
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
/-- The algebra norm `algNormOfAlgEquiv` is nonarchimedean.  -/
IsUltrametricDist.isNonarchimedean_algNormOfAlgEquiv : ∀ {K : Type u_1} [inst : NormedField K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : Gal(L/K)),
  IsNonarchimedean ⇑(IsUltrametricDist.algNormOfAlgEquiv σ)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheoremKind.isDefault : Lean.Meta.Grind.EMatchTheoremKind → Bool
-- Init.Data.List.Perm
List.singleton_perm : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Perm l ↔ [a] = l
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_eq_iteratedDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜},
  UniqueDiffOn 𝕜 s → ContDiffAt 𝕜 (↑n) f x → x ∈ s → iteratedDerivWithin n f s x = iteratedDeriv n f x
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_one : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V), ⇑1 = id
-- Batteries.Data.BitVec.Lemmas
BitVec.getMsb_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool) (i : Fin n), (BitVec.ofFnBE f).getMsb i = f i
-- Mathlib.RingTheory.PowerSeries.CoeffMulMem
PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal : ∀ {A : Type u_1} [inst : Semiring A] {I J : Ideal A} {f g : PowerSeries A} (n : ℕ),
  (∀ i ≤ n, (PowerSeries.coeff i) f ∈ I) →
    (∀ i ≤ n, (PowerSeries.coeff i) g ∈ J) → ∀ i ≤ n, (PowerSeries.coeff i) (f * g) ∈ I * J
-- Mathlib.Data.Ordmap.Invariants
/-- Build a tree from three nodes, left associated (ignores the invariants).  -/
Ordnode.node3L : {α : Type u_1} → Ordnode α → α → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.prodFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D') (f : CategoryTheory.StructuredArrow (S, S') (T.prod T')),
  (CategoryTheory.StructuredArrow.prodFunctor S S' T T').obj f =
    (CategoryTheory.StructuredArrow.mk f.hom.1, CategoryTheory.StructuredArrow.mk f.hom.2)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : FreeGroup α), x.norm = x.toWord.length
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Any cone morphism between limit cones is an isomorphism.  -/
CategoryTheory.Limits.IsLimit.hom_isIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t) (f : s ⟶ t), CategoryTheory.IsIso f
-- Mathlib.Algebra.Group.Int.Defs
Int.instAddSemigroup : AddSemigroup ℤ
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l).get k' h = k
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmooth.of_algEquiv : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_1}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T) [Algebra.IsStandardSmooth R S],
  Algebra.IsStandardSmooth R T
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_sub_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (c : F),
  derivWithin (fun y => f y - c) s x = derivWithin f s x
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.toCWComplex_map : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [inst_1 : Topology.RelCWComplex C ∅] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Topology.CWComplex.map n i = Topology.RelCWComplex.map n i
-- Mathlib.Data.Quot
/-- Descends a function `f : α → β → γ` to quotients of `α` and `β` and applies it.  -/
Quot.liftOn₂ : {α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_4} →
      {r : α → α → Prop} →
        {s : β → β → Prop} →
          Quot r →
            Quot s →
              (f : α → β → γ) →
                (∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) →
                  (∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b) → γ
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_of_apply_add : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddRightCancelMonoid ι] [inst_5 : SetLike.GradedMonoid A]
  (r : DirectSum ι fun i => ↥(A i)) {i : ι} (r' : ↥(A i)) (j : ι),
  ↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') (j + i)) = ↑(r j) * ↑r'
-- Mathlib.Algebra.Category.Ring.Basic
/-- The forgetful functor from `CommSemiRingCat` to `SemiRingCat` is fully faithful.  -/
CommSemiRingCat.fullyFaithfulForget₂ToSemiRingCat : (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).FullyFaithful
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.evalTermWithRef : {α : Type} → [Lean.Elab.ConfigEval.EvalTerm α] → Lean.Term → Lean.Elab.TermElabM α
-- Mathlib.Analysis.Normed.Module.Complemented
/-- If `q` is a closed complement of a closed subspace `p`, then `p × q` is continuously
isomorphic to `E`.  -/
Submodule.prodEquivOfClosedCompl : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [CompleteSpace E] → (p q : Subspace 𝕜 E) → IsCompl p q → IsClosed ↑p → IsClosed ↑q → (↥p × ↥q) ≃L[𝕜] E
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt64.size ≤ n → (UInt64.ofNatClamp n).toNat = UInt64.size - 1
-- Mathlib.Tactic.Positivity.Basic
/-- **Alias** of the reverse direction of `NNRat.num_pos`. -/
Mathlib.Meta.Positivity.NNRat.num_pos_of_pos : ∀ {q : ℚ≥0}, 0 < q → 0 < q.num
-- Mathlib.Algebra.GroupWithZero.Range
/-- For a morphism of monoids with zero `f`, this is a smallest submonoid of the invertible
elements in the codomain containing the range of `f`.  -/
MonoidWithZeroHom.valueMonoid : {A : Type u_1} → {B : Type u_2} → [inst : MonoidWithZero A] → [inst_1 : MonoidWithZero B] → (A →*₀ B) → Submonoid Bˣ
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
CategoryTheory.Limits.instHasFiniteLimitsFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Functor K C)
-- Mathlib.Algebra.Category.Ring.Limits
/-- The category of rings has all limits.  -/
CommSemiRingCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommSemiRingCat
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_app.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  (ℌ : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H),
  ℌ.ev_app =
    (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy F H).homEquiv.symm
      { app := fun x => CategoryTheory.MonoidalClosed.uncurry (ℌ.π x.2 x.1), naturality := ⋯ }
-- Mathlib.FieldTheory.CardinalEmb
/-- Index a basis of E/F using the initial ordinal of the cardinal `Module.rank F E`.  -/
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.termι : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainNonUnitalRingHom.eq_1 : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N] (f : M →ₙ* N),
  MonoidAlgebra.mapDomainNonUnitalRingHom R f =
    { toFun := MonoidAlgebra.mapDomain ⇑f, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.NormalizedHom.cons.sizeOf_spec : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₁) (a : Mathlib.Tactic.BicategoryLike.NormalizedHom)
  (a_1 : Mathlib.Tactic.BicategoryLike.Atom₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.NormalizedHom.cons e a a_1) = 1 + sizeOf e + sizeOf a + sizeOf a_1
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppLevel : Lean.Level → Lean.MetaM Std.Format
-- Mathlib.Analysis.Calculus.DSlope
sub_smul_dslope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (a b : 𝕜), (b - a) • dslope f a b = f b - f a
-- Init.Data.List.Find
List.isSome_idxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, (List.idxOf? a l).isSome = true ↔ a ∈ l
-- Mathlib.Topology.Constructions
instTopologicalSpaceQuot : {X : Type u} → {r : X → X → Prop} → [t : TopologicalSpace X] → TopologicalSpace (Quot r)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.MorphismProperty.LeftFraction₂.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Y' : C}
  (f f_1 : X ⟶ Y'),
  f = f_1 →
    ∀ (f' f'_1 : X ⟶ Y'),
      f' = f'_1 →
        ∀ (s s_1 : Y ⟶ Y') (e_s : s = s_1) (hs : W s),
          { Y' := Y', f := f, f' := f', s := s, hs := hs } = { Y' := Y', f := f_1, f' := f'_1, s := s_1, hs := ⋯ }
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.Cotangent.smul_eq_zero_of_mem : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {x : R}, x ∈ I → ∀ (m : I.Cotangent), x • m = 0
-- Init.Data.Int.Lemmas
Int.ofNat_sub : ∀ {m n : ℕ}, m ≤ n → ↑(n - m) = ↑n - ↑m
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.vaddAntidiagonal_mono_right : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s : Set G} {t v : Set P} (a : P)
  (hst : (s.vaddAntidiagonal t a).Finite) (hsv : (s.vaddAntidiagonal v a).Finite),
  v ⊆ t → Finset.VAddAntidiagonal a hsv ⊆ Finset.VAddAntidiagonal a hst
-- Mathlib.Topology.Instances.Nat
Nat.dist_coe_int : ∀ (x y : ℕ), dist ↑x ↑y = dist x y
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.trailingNode.parenthesizer : Lean.SyntaxNodeKind → ℕ → ℕ → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instInv.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Inv (G i)], Pi.instInv = { inv := fun f i => (f i)⁻¹ }
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instFullTopCatToTopCat : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)], (ContinuousGeneratedByCat.toTopCat X).Full
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_diff!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff! m₂).getKey! k = m₁.getKey! k
-- Mathlib.RingTheory.Flat.Rank
Module.rankAtStalk_pos_iff_algebraMap_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S], (∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p) ↔ Function.Injective ⇑(algebraMap R S)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instIsSmallInnerHornInclusions : CategoryTheory.MorphismProperty.IsSmall.{u, u, u + 1} SSet.innerHornInclusions
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_le_size_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β}, t.size - 1 ≤ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.size
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {u : Set M'} {y : M'},
  MDiffAt[u] g y → MDiffAt[s] f x → f ⁻¹' u ∈ nhdsWithin x s → f x = y → MDiffAt[s] (g ∘ f) x
-- Init.Data.List.Lemmas
List.exists_mem_iff_exists_getElem : ∀ {α : Type u_1} {P : α → Prop} {l : List α}, (∃ x ∈ l, P x) ↔ ∃ i, ∃ (hi : i < l.length), P l[i]
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- The elements `1, x, ..., x ^ (d - 1)` form a basis for `K⟮x⟯`,
where `d` is the degree of the minimal polynomial of `x`.  -/
IntermediateField.powerBasisAux : {K : Type u} →
  [inst : Field K] →
    {L : Type u_3} →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → {x : L} → IsIntegral K x → Module.Basis (Fin (minpoly K x).natDegree) K ↥K⟮x⟯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.forIn.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [inst : Monad m]
  [inst_1 : LawfulMonad m] [inst_2 : Std.TransCmp cmp] (f f_1 : α → β → δ → m (ForInStep δ)),
  f = f_1 →
    ∀ (init init_1 : δ),
      init = init_1 →
        ∀ (t t_1 : Std.ExtTreeMap α β cmp),
          t = t_1 → Std.ExtTreeMap.forIn f init t = Std.ExtTreeMap.forIn f_1 init_1 t_1
-- Mathlib.Topology.Defs.Induced
/-- A function `f : X → Y` between topological spaces is coinducing if the topology on `Y` is
coinduced by the topology on `X` through `f`, meaning that a set `s : Set Y` is open iff its
preimage is open.  -/
Topology.IsCoinducing : {X : Type u_1} → {Y : Type u_2} → [tX : TopologicalSpace X] → [tY : TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If `g` (semi)conjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
of `fb`.  -/
Function.IsFixedPt.map : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {x : α},
  Function.IsFixedPt fa x → ∀ {g : α → β}, Function.Semiconj g fa fb → Function.IsFixedPt fb (g x)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The functor from `C` to `Over (𝟙_ C)` which sends `X : C` to `Over.mk <| toUnit X`.  -/
CategoryTheory.toOverUnit : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.Algebra.GroupWithZero.Associated
DvdNotUnit.not_associated : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p q : M}, DvdNotUnit p q → ¬Associated p q
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.mk.injEq : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (toNonUnitalRingHom : A →ₙ+* B)
  (map_star' : ∀ (a : A), toNonUnitalRingHom.toFun (star a) = star (toNonUnitalRingHom.toFun a))
  (toNonUnitalRingHom_1 : A →ₙ+* B)
  (map_star'_1 : ∀ (a : A), toNonUnitalRingHom_1.toFun (star a) = star (toNonUnitalRingHom_1.toFun a)),
  ({ toNonUnitalRingHom := toNonUnitalRingHom, map_star' := map_star' } =
      { toNonUnitalRingHom := toNonUnitalRingHom_1, map_star' := map_star'_1 }) =
    (toNonUnitalRingHom = toNonUnitalRingHom_1)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.typeOf.congr_simp : ∀ {L : FirstOrder.Language} (T : L.Theory) {α : Type w} {M : Type w'} [inst : L.Structure M] [inst_1 : Nonempty M]
  [inst_2 : M ⊨ T] (v v_1 : α → M), v = v_1 → T.typeOf v = T.typeOf v_1
-- Mathlib.RingTheory.Perfection
Perfection.hom_ext : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {R : Type u₁} [inst : CommSemiring R] [CharP R p] [PerfectRing R p] {S : Type u₂}
  [inst_3 : CommSemiring S] [inst_4 : CharP S p] {f g : R →+* Perfection S p},
  (∀ (x : R), (Perfection.coeff S p 0) (f x) = (Perfection.coeff S p 0) (g x)) → f = g
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
TensorialAt.mkHom₂_apply : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {F' : Type u_7}
  [inst_13 : NormedAddCommGroup F'] [inst_14 : NormedSpace 𝕜 F'] {V' : M → Type u_8}
  [inst_15 : TopologicalSpace (Bundle.TotalSpace F' V')] [inst_16 : (x : M) → AddCommGroup (V' x)]
  [inst_17 : (x : M) → Module 𝕜 (V' x)] [inst_18 : (x : M) → TopologicalSpace (V' x)] [inst_19 : FiberBundle F' V']
  {A : Type u_9} [inst_20 : AddCommGroup A] [inst_21 : Module 𝕜 A] [inst_22 : VectorBundle 𝕜 F V]
  [inst_23 : VectorBundle 𝕜 F' V'] [inst_24 : CompleteSpace 𝕜] [inst_25 : FiniteDimensional 𝕜 F]
  [inst_26 : FiniteDimensional 𝕜 F'] [inst_27 : ContMDiffVectorBundle 1 F V I]
  [inst_28 : ContMDiffVectorBundle 1 F' V' I] [inst_29 : TopologicalSpace A] [inst_30 : IsTopologicalAddGroup A]
  [inst_31 : ContinuousSMul 𝕜 A] {Φ : ((x : M) → V x) → ((x : M) → V' x) → A} {x : M}
  (hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x => Φ x τ) x)
  (hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x) {σ : (x : M) → V x},
  MDiffAt (T% σ) x → ∀ {τ : (x : M) → V' x}, MDiffAt (T% τ) x → ⋯ = Φ σ τ
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Cardinal.iSup_lt_of_lt_cof_ord`. -/
Ordinal.iSup_lt : ∀ {α : Type u} {f : α → Cardinal.{u}} {a : Cardinal.{u}},
  Cardinal.mk α < a.ord.cof → (∀ (i : α), f i < a) → ⨆ i, f i < a