mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry'_ihom_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.Closed X] (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry' f) ((CategoryTheory.ihom X).map g) =
    CategoryTheory.MonoidalClosed.curry' (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_pow_right`. -/
Equiv.Perm.SameCycle.pow_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℕ}, f.SameCycle x y → f.SameCycle x ((f ^ n) y)
-- Mathlib.Tactic.Choose
/-- `mkFreshNameFrom orig base` returns `mkFreshUserName base` if ``orig = `_``
and `orig` otherwise.  -/
Mathlib.Tactic.Choose.mkFreshNameFrom : Lean.Name → Lean.Name → Lean.CoreM Lean.Name
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {n : ℕ}, q ^ n ∣ p → q ^ (n - 1) ∣ Polynomial.derivative p
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.mk.sizeOf_spec : ∀ (fvarId : Lean.FVarId) (userName : Lean.Name) (id : Lean.Meta.Origin) (origType type proof : Lean.Expr),
  sizeOf { fvarId := fvarId, userName := userName, id := id, origType := origType, type := type, proof := proof } =
    1 + sizeOf fvarId + sizeOf userName + sizeOf id + sizeOf origType + sizeOf type + sizeOf proof
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nat_mul_two_pi_sub : ∀ (x : ℝ) (n : ℕ), Real.cos (↑n * (2 * Real.pi) - x) = Real.cos x
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
CommGrpCat.μ_forget_apply : ∀ {G H : CommGrpCat} (p : ↑G) (q : ↑H),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget CommGrpCat) G H))
      (p, q) =
    (p, q)
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.instDiv : {𝕜 : Type u_1} → [inst : NormedDivisionRing 𝕜] → Div ↑(Metric.sphere 0 1)
-- Mathlib.LinearAlgebra.Complex.Module
Complex.range_liftAux : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] (I' : A) (hI' : I' * I' = -1),
  (Complex.liftAux I' hI').range = ℝ[I']
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_abs_right`. -/
Asymptotics.IsBigO.abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
  f =O[l] u → f =O[l] fun x => |u x|
-- Mathlib.Control.ULift
/-- Functorial action.  -/
PLift.map : {α : Sort u} → {β : Sort v} → (α → β) → PLift α → PLift β
-- Mathlib.Topology.DiscreteSubset
IsCompact.codiscreteWithin_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {K : Set X} [T1Space X],
  IsCompact K → Filter.codiscreteWithin K = Filter.cofinite ⊓ Filter.principal K
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.preservesCokernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) L
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Measurable.ereal_exp : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → EReal}, Measurable f → Measurable fun x => (f x).exp
-- Init.Grind.ToIntLemmas
_private.Init.Grind.ToIntLemmas.0.Lean.Grind.IntInterval.lo?.match_1.eq_4 : ∀ (motive : Lean.Grind.IntInterval → Sort u_1) (h_1 : (lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi))
  (h_2 : (lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) (h_3 : (hi : ℤ) → motive (Lean.Grind.IntInterval.io hi))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii),
  (match Lean.Grind.IntInterval.ii with
    | Lean.Grind.IntInterval.co lo hi => h_1 lo hi
    | Lean.Grind.IntInterval.ci lo => h_2 lo
    | Lean.Grind.IntInterval.io hi => h_3 hi
    | Lean.Grind.IntInterval.ii => h_4 ()) =
    h_4 ()
-- Init.Data.Option.Lemmas
Option.le.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (val : β), Option.le r none (some val) = True
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.strongAnodyneExtensions_le_anodyneExtensions : SSet.strongAnodyneExtensions ≤ SSet.anodyneExtensions
-- Mathlib.Data.UInt
USize.toBitVec_zsmul : ∀ (z : ℤ) (a : USize), (z • a).toBitVec = z • a.toBitVec
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_disjointOfDiffUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), (↑I).PairwiseDisjoint id → (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.iSup_basicOpen_eq_top_iff : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_1} {f : ι → R},
  ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤
-- Mathlib.CategoryTheory.Balanced
CategoryTheory.isIso_iff_mono_and_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Balanced C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ CategoryTheory.Mono f ∧ CategoryTheory.Epi f
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- A set `S` of continuous linear maps is von Neumann bounded
iff for any von Neumann bounded set `s`,
the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded.

For the forward implication with weaker typeclass assumptions, see `isVonNBounded_image2_apply`.  -/
ContinuousLinearMap.isVonNBounded_iff : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] {R : Type u_7} [inst_7 : NormedDivisionRing R] [inst_8 : TopologicalSpace F]
  [inst_9 : IsTopologicalAddGroup F] [inst_10 : Module R F] [inst_11 : ContinuousConstSMul R F]
  [inst_12 : SMulCommClass 𝕜₂ R F] {S : Set (E →SL[σ] F)},
  Bornology.IsVonNBounded R S ↔
    ∀ (s : Set E), Bornology.IsVonNBounded 𝕜₁ s → Bornology.IsVonNBounded R (Set.image2 (fun f x => f x) S s)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.instGroupGal : {F : Type u_1} → [inst : Field F] → (p : Polynomial F) → Group p.Gal
-- Mathlib.Topology.NhdsWithin
frequently_nhdsWithin_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {z : α} {s : Set α} {p : α → Prop},
  (∃ᶠ (x : α) in nhdsWithin z s, p x) ↔ ∃ᶠ (x : α) in nhds z, p x ∧ x ∈ s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → (t.insertIfNew k v).minKey? = some k
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpi.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : Y ⟶ X},
  Nonempty (CategoryTheory.EffectiveEpiStruct f) → CategoryTheory.EffectiveEpi f
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeGPFree_insert : ∀ {α : Type u_2} [inst : CommMonoid α] [IsCancelMul α] {s : Set α} {a : α},
  ThreeGPFree (insert a s) ↔
    ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getThenInsertIfNew?_snd : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (Std.DTreeMap.Raw.Const.getThenInsertIfNew? t k v).2 = t.insertIfNew k v
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.toList.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Batteries.AssocList α β → Sort u_3) (a : α) (b : β)
  (es : Batteries.AssocList α β) (h_1 : Unit → motive Batteries.AssocList.nil)
  (h_2 : (a : α) → (b : β) → (es : Batteries.AssocList α β) → motive (Batteries.AssocList.cons a b es)),
  (match Batteries.AssocList.cons a b es with
    | Batteries.AssocList.nil => h_1 ()
    | Batteries.AssocList.cons a b es => h_2 a b es) =
    h_2 a b es
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  [inst_2 : DistribSMul R α] [SMulCommClass R α α] (v : m → α) (b : R) (M : Matrix m n α),
  Matrix.vecMul v (b • M) = b • Matrix.vecMul v M
-- Mathlib.GroupTheory.Perm.Support
/-- `f.IsSwap` indicates that the permutation `f` is a transposition of two elements.  -/
Equiv.Perm.IsSwap : {α : Type u_1} → [DecidableEq α] → Equiv.Perm α → Prop
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.comap_comap : ∀ {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter γ) {m : α → β} {n : β → γ} (inj₀ : Function.Injective n)
  (large₀ : Set.range n ∈ f) (inj₁ : Function.Injective m) (large₁ : Set.range m ∈ f.comap inj₀ large₀)
  (inj₂ : optParam (Function.Injective (n ∘ m)) ⋯) (large₂ : optParam (Set.range (n ∘ m) ∈ f) ⋯),
  (f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Directed.ciInf_le : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] {f : ι → α},
  Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → ∀ (i : ι), ⨅ j, f j ≤ f i
-- Mathlib.RingTheory.Polynomial.Chebyshev
_private.Mathlib.RingTheory.Polynomial.Chebyshev.0.Polynomial.Chebyshev.T.match_1.eq_3 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (n : ℕ) → motive (Int.ofNat n.succ.succ)) (h_4 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | Int.ofNat n.succ.succ => h_3 n
    | Int.negSucc n => h_4 n) =
    h_3 n
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- The smallest σ-algebra containing a collection `s` of basic sets  -/
MeasurableSpace.GenerateMeasurable : {α : Type u_1} → Set (Set α) → Set α → Prop
-- Mathlib.Tactic.ToExpr
/-- Core of a hand-written `ToExpr` handler for `MData`.
Uses the `KVMap.set*` functions rather than going into the internals
of the `KVMap` data structure.  -/
_private.Mathlib.Tactic.ToExpr.0.Mathlib.toExprMData : Lean.MData → Lean.Expr
-- Lean.Meta.Sym.Eta
/-- Returns `true` if `e` contains a loose bound variable with index in `[0, n)`
This function assumes `n` is small. If this becomes a bottleneck, we should
implement a version of `lean_expr_has_loose_bvar` that checks the range in one traversal.
 -/
_private.Lean.Meta.Sym.Eta.0.Lean.Meta.Sym.hasLooseBVarsInRange : Lean.Expr → ℕ → Bool
-- Mathlib.Data.Set.Lattice
Set.sUnion_symmDiff_subset : ∀ {α : Type u_1} {s : Set α} {S : Set (Set α)}, S.Nonempty → symmDiff (⋃₀ S) s ⊆ ⋃₀ ((fun x => symmDiff x s) '' S)
-- Mathlib.Order.Lex
instLawfulBEqLex : ∀ (α : Type u_2) [inst : BEq α] [LawfulBEq α], LawfulBEq (Lex α)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.basisOf_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V]
  [inst_1 : AddTorsor V P] [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι') (i : ι'),
  (b.reindex e).basisOf i = (b.basisOf (e.symm i)).reindex (e.subtypeEquiv ⋯)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.pure_one : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], Interval.pure 1 = 1
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.ψ₂.eq_1 : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (w : X ⟶ Y) (hw : W w),
  CategoryTheory.Localization.Construction.ψ₂ W w hw =
    (CategoryTheory.Paths.of (CategoryTheory.Localization.Construction.LocQuiver W)).map (Sum.inr ⟨w, hw⟩)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mulActionHom_compl_bijective : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α]
  [inst_3 : Fintype α] {m : ℕ} (hm : m + n = Fintype.card α),
  Function.Bijective ⇑(Set.powersetCard.mulActionHom_compl G α hm)
-- Lean.Widget.UserWidget
Lean.Widget.WidgetSource.mk.sizeOf_spec : ∀ (sourcetext : String), sizeOf { sourcetext := sourcetext } = 1 + sizeOf sourcetext
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roc_eq_some : ∀ {m n i : ℕ}, i < n - m → (m<...=n).toList[i]? = some (m + 1 + i)
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.ExtendingEntrypoint : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Type
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMul.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G]
  [toIsManifold : IsManifold I n G], (ContMDiff (I.prod I) I n fun p => p.1 * p.2) → ContMDiffMul I n G
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i))
  (T : CategoryTheory.Limits.FormalCoproduct C)
  (s : { p // CategoryTheory.CategoryStruct.comp p.1 f = CategoryTheory.CategoryStruct.comp p.2 g }) (i : T.I),
  ((CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv f g pb hpb T).symm s).φ i =
    (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (CategoryTheory.Limits.PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instNonemptyMethodsRef : Nonempty Lean.Meta.Grind.MethodsRef
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_add : ∀ {R : Type u_1} (n : ℕ) [inst : Semiring R] (r s : R),
  (SkewPolynomial.monomial n) (r + s) = (SkewPolynomial.monomial n) r + (SkewPolynomial.monomial n) s
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_false : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α},
  (Filter.blimsup u f fun x => False) = ⊥
-- Mathlib.Order.Filter.Basic
Filter.isGLB_sInf : ∀ {α : Type u} (s : Set (Filter α)), IsGLB s (sInf s)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.takeWhile.match_1.splitter : (motive : Substring.Raw → (Char → Bool) → Sort u_1) →
  (x : Substring.Raw) →
    (x_1 : Char → Bool) →
      ((s : String) → (b e : String.Pos.Raw) → (p : Char → Bool) → motive { str := s, startPos := b, stopPos := e } p) →
        motive x x_1
-- Mathlib.RingTheory.Derivation.MapCoeffs
/-- `algEquiv_deriv` in a separable algebra
 -/
Differential.algEquiv_deriv' : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] {R : Type u_2} [inst_2 : CommRing R]
  [inst_3 : Differential R] [inst_4 : Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [inst_6 : CommRing R']
  [inst_7 : Differential R'] [inst_8 : Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] [Algebra.IsSeparable A R]
  (f : R ≃ₐ[A] R') (x : R), f x′ = (f x)′
-- Mathlib.Data.Set.Prod
Set.update_preimage_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [inst : DecidableEq ι]
  {f : (i : ι) → α i}, i ∈ s → (∀ j ∈ s, j ≠ i → f j ∈ t j) → Function.update f i ⁻¹' s.pi t = t i
-- Mathlib.Order.Partition.Finpartition
Finpartition.nonempty_of_mem_parts : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : Finset α}, a ∈ P.parts → a.Nonempty
-- Mathlib.Geometry.Euclidean.Altitude
/-- The inner product of two distinct altitudes has absolute value strictly less than the product of
their lengths.

Equivalently, neither vector is a multiple of the other; the angle between them is not 0 or π.  -/
Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mul : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) [inst_4 : n.AtLeastTwo] {i j : Fin (n + 1)},
  i ≠ j → |inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j)| < s.height i * s.height j
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Type
-- Mathlib.Order.Filter.Basic
Filter.eventually_inf_principal : ∀ {α : Type u} {f : Filter α} {p : α → Prop} {s : Set α},
  (∀ᶠ (x : α) in f ⊓ Filter.principal s, p x) ↔ ∀ᶠ (x : α) in f, x ∈ s → p x
-- Init.Data.Bool
Bool.true_eq : ∀ (b : Bool), (true = b) = (b = true)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
cfcHomSuperset.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {p p_1 : A → Prop} (e_p : p = p_1) [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A]
  [instCFC : ContinuousFunctionalCalculus R A p] {a a_1 : A} (e_a : a = a_1) (ha : p a) {s : Set R}
  (hs : spectrum R a ⊆ s), cfcHomSuperset ha hs = cfcHomSuperset ⋯ ⋯
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Construct a linear map from a function `f` satisfying `IsBoundedLinearMap 𝕜 f`.  -/
IsBoundedLinearMap.toLinearMap : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring 𝕜] →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : SeminormedAddCommGroup F] →
              [inst_4 : Module 𝕜 F] → (f : E → F) → IsBoundedLinearMap 𝕜 f → E →ₗ[𝕜] F
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.toPiFork_π_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I)
  {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right}
  (hd : CategoryTheory.Limits.IsLimit d),
  (CategoryTheory.Limits.Multifork.toPiFork hc hd K).ι = CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.isComplemented_iff : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α},
  ComplementedLattice ↥L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- The ring homomorphism from the quotient by a smaller ideal to the quotient by a larger ideal.

This is the `Ideal.Quotient` version of `Quot.Factor`

When the two ideals are of the form `I^m` and `I^n` and `n ≤ m`,
please refer to the dedicated version `Ideal.Quotient.factorPow`.  -/
Ideal.Quotient.factor : {R : Type u} →
  [inst : Ring R] → {S T : Ideal R} → [inst_1 : S.IsTwoSided] → [inst_2 : T.IsTwoSided] → S ≤ T → R ⧸ S →+* R ⧸ T
-- Mathlib.Data.Seq.Computation
Computation.liftRel_think_right : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β),
  Computation.LiftRel R ca cb.think ↔ Computation.LiftRel R ca cb
-- Mathlib.RingTheory.Teichmuller
Perfection.quotientMulEquiv.eq_1 : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {R : Type u_2} [inst_1 : CommRing R] (I : Ideal R) [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R],
  Perfection.quotientMulEquiv p I =
    (Perfection.mapMonoidHom p ↑(Ideal.Quotient.mk I)).toMulEquiv
      ((Perfection.liftMonoidHom p (Perfection (R ⧸ I) p) R) (Perfection.teichmuller p I)) ⋯ ⋯
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.n : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.Iterators.Types.StepSizeIterator α m β → ℕ
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.SignedMeasure.toComplexMeasure_apply_im : ∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α) (i : Set α),
  ((s.toComplexMeasure t).measureOf' i).im = t i
-- Init.Control.Lawful.Instances
ExceptT.ext_iff : ∀ {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x y : ExceptT ε m α}, x = y ↔ x.run = y.run
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.CofibrantObject.localizerMorphism C).IsLocalizedEquivalence
-- Init.Data.SInt.Lemmas
Int8.ofInt_eq_iff_bmod_eq_toInt : ∀ (a : ℤ) (b : Int8), Int8.ofInt a = b ↔ a.bmod (2 ^ 8) = b.toInt
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM.Context.opId : Lean.Meta.Grind.AC.ACM.Context → ℕ
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
HomotopyCategory.Plus.quasiIso_eq_subcategoryAcyclic_trW : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  HomotopyCategory.Plus.quasiIso C = (HomotopyCategory.Plus.subcategoryAcyclic C).trW
-- Init.Data.Order.Classes
Std.IsLinearOrder.toIsLinearPreorder : ∀ {α : Type u} [inst : LE α] [self : Std.IsLinearOrder α], Std.IsLinearPreorder α
-- Lean.Data.Lsp.Extra
Lean.Lsp.ModuleHierarchyOptions : Type
-- Mathlib.Lean.MessageData.Trace
/-- Strip the leading status emoji and space from a trace header string,
leaving just the semantic content for comparison across trace runs.

Trace headers from `withTraceNode` have the form `"{emoji}[{VS16}] {content}"`.
This strips everything through the first space. Returns the string unchanged if
no recognized status prefix is present.  -/
Lean.MessageData.stripTraceResultPrefix : String → String
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheorems.mk.sizeOf_spec : ∀
  (theorems :
    Std.HashMap (Lean.Name × Mathlib.Meta.FunProp.LambdaTheoremType) (Array Mathlib.Meta.FunProp.LambdaTheorem)),
  sizeOf { theorems := theorems } = 1 + sizeOf theorems
-- Init.Data.Order.PackageFactories
Std.PartialOrderPackage.ofLE : (α : Type u) →
  autoParam (Std.Packages.PartialOrderOfLEArgs α) Std.PartialOrderPackage.ofLE._auto_1 → Std.PartialOrderPackage α
-- Mathlib.Data.Int.Init
Int.succ_neg_natCast_succ : ∀ (n : ℕ), (-↑n.succ).succ = -↑n
-- Aesop.Tree.Traversal
Aesop.traverseDown : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT (ST IO.RealWorld) m] →
      (Aesop.GoalRef → m Bool) →
        (Aesop.GoalRef → m Unit) →
          (Aesop.RappRef → m Bool) →
            (Aesop.RappRef → m Unit) →
              (Aesop.MVarClusterRef → m Bool) → (Aesop.MVarClusterRef → m Unit) → Aesop.TreeRef → m Unit
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.a'.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a a_1 : Matrix α β (NumberField.RingOfIntegers K)),
  a = a_1 →
    ∀ (a_2 a_3 : α),
      a_2 = a_3 →
        ∀ (a_4 a_5 : β),
          a_4 = a_5 →
            ∀ (a_6 a_7 : K →+* ℂ),
              a_6 = a_7 →
                ∀ (a_8 a_9 : K →+* ℂ),
                  a_8 = a_9 → NumberField.house.a'✝ K a a_2 a_4 a_6 a_8 = NumberField.house.a'✝ K a_1 a_3 a_5 a_7 a_9
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.minimalPrimes_eq_subsingleton : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, I.IsPrimary → I.minimalPrimes = {I.radical}