mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filter_key_equiv_self_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → Bool},
  Std.ExtDHashMap.filter (fun k x => f k) m = m ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = true
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_erase_le_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k km kme : α}
  (hkme : (t.erase k).max? = some kme), t.max?.get ⋯ = km → (cmp kme km).isLE = true
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The preimage of an open normal subgroup under a morphism to a profinite group.  -/
ProfiniteGrp.ProfiniteCompletion.preimage : {G : GrpCat} →
  {P : ProfiniteGrp.{u}} →
    (G ⟶ GrpCat.of ↑P.toProfinite.toTop) → OpenNormalSubgroup ↑P.toProfinite.toTop → FiniteIndexNormalSubgroup ↑G
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabCharLit : Lean.Elab.Term.TermElab
-- Batteries.Data.Char.AsciiCasing
Char.isLower_toUpper_eq_false : ∀ (c : Char), c.toUpper.isLower = false
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mul : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (self : CategoryTheory.Subgroupoid C) {c d e : C} {p : c ⟶ d},
  p ∈ self.arrows c d → ∀ {q : d ⟶ e}, q ∈ self.arrows d e → CategoryTheory.CategoryStruct.comp p q ∈ self.arrows c e
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.integrable_kernel_prodMk_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] (a : α) {s : Set (β × γ)},
  MeasurableSet s →
    ((κ.compProd η) a) s ≠ ⊤ → MeasureTheory.Integrable (fun b => (η (a, b)).real (Prod.mk b ⁻¹' s)) (κ a)
-- Mathlib.Algebra.MvPolynomial.Counit
/-- `MvPolynomial.counit R` is the natural surjective ring homomorphism
`MvPolynomial R ℤ →+* R` obtained by `X r ↦ r`.

See `MvPolynomial.ACounit` for a “relative” variant for algebras over a base ring,
and `MvPolynomial.counitNat` for the “absolute” variant with `R = ℕ`.  -/
MvPolynomial.counit : (R : Type u_3) → [inst : CommRing R] → MvPolynomial R ℤ →+* R
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  (I : FractionalIdeal (nonZeroDivisors R) K),
  FractionalIdeal.absNorm I = ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|
-- Mathlib.Data.Finsupp.Order
Finsupp.embDomain_tsub : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : CanonicallyOrderedAdd α] [inst_3 : Sub α] [inst_4 : OrderedSub α] (f : ι ↪ κ) (f1 f2 : ι →₀ α),
  Finsupp.embDomain f (f1 - f2) = Finsupp.embDomain f f1 - Finsupp.embDomain f f2
-- Mathlib.Order.Heyting.Basic
sdiff_right_comm : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (c b a : α), (c \ b) \ a = (c \ a) \ b
-- Mathlib.Order.GameAdd
Prod.gameAdd_iff : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {x y : α × β},
  Prod.GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensLegend.mk.sizeOf_spec : ∀ (tokenTypes tokenModifiers : Array String),
  sizeOf { tokenTypes := tokenTypes, tokenModifiers := tokenModifiers } = 1 + sizeOf tokenTypes + sizeOf tokenModifiers
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.algebraMap_def' : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (r : R), (algebraMap R (GradedTensorProduct R 𝒜 ℬ)) r = 1 ᵍ⊗ₜ[R] (algebraMap R B) r
-- Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
/-- Key lemma towards the Erdős-Kaplansky theorem from https://mathoverflow.net/a/168624  -/
max_aleph0_card_le_rank_fun_nat : ∀ (K : Type u) [inst : DivisionRing K], max Cardinal.aleph0 (Cardinal.mk K) ≤ Module.rank K (ℕ → K)
-- Mathlib.Data.Int.CardIntervalMod
/-- There are `b / r + [v % r < b % r]` numbers in `[0, b)` congruent to `v` mod `r`,
where `[·]` is the Iverson bracket.  -/
Nat.count_modEq_card : ∀ (b : ℕ) {r : ℕ}, 0 < r → ∀ (v : ℕ), Nat.count (fun x => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.preΨ_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [Nontrivial R] {n : ℤ}, ↑n ≠ 0 → W.preΨ n ≠ 0
-- Mathlib.Data.Finset.Option
Finset.some_mem_insertNone : ∀ {α : Type u_1} {s : Finset α} {a : α}, some a ∈ Finset.insertNone s ↔ a ∈ s
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hV1 : {k : Type u} →
  {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → (self : Rep.{w, u, v} k G) → AddCommGroup ↑self
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderUnitor.rightUnitor_inv_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  (P : CategoryTheory.MorphismProperty C) [self : P.IsStableUnderUnitor] (c : C),
  P (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).inv
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Nat.Subtype.toFunAux.eq_1 : ∀ {s : Set ℕ} [inst : DecidablePred fun x => x ∈ s] (x : ↑s),
  Nat.Subtype.toFunAux✝ x = List.countP (fun x => decide (x ∈ s)) (List.range ↑x)
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_apply : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] (x : α), normalize x = x * ↑(normUnit x)
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a finite set `s`, the sum of `f i / g i` over `i ∈ s` equals the sum of `f i`
over `i ∈ s` minus the sum of `g i` over `i ∈ s`.  -/
finsum_mem_sub_distrib : ∀ {α : Type u_1} {G : Type u_4} {s : Set α} [inst : SubtractionCommMonoid G] (f g : α → G),
  s.Finite → ∑ᶠ (i : α) (_ : i ∈ s), (f i - g i) = ∑ᶠ (i : α) (_ : i ∈ s), f i - ∑ᶠ (i : α) (_ : i ∈ s), g i
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.isomorphisms_le_of_containsIdentities : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.ContainsIdentities]
  [P.RespectsIso], CategoryTheory.MorphismProperty.isomorphisms C ≤ P
-- Init.Meta.Defs
/-- Syntax that represents a Lean term.
 -/
Lean.Syntax.Term : Type
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [hw : w.GuitartExact] (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- If `a` is in `integerSet`, then there is a *unique* algebraic integer in `𝓞 K` such
that `mixedEmbedding K x = a`.  -/
NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {a : NumberField.mixedEmbedding.mixedSpace K},
  a ∈ NumberField.mixedEmbedding.fundamentalCone.integerSet K → ∃! x, (NumberField.mixedEmbedding K) ↑x = a
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B),
  (CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).map f = f.val
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited α] {f : α → β → Bool} {k : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filter f m).getKey! k =
    ((m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)).get!
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MonadHorizontalComp.toMonadWhiskerRight : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadHorizontalComp m] → Mathlib.Tactic.BicategoryLike.MonadWhiskerRight m
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_eq_lintegral_klFun_of_ac : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    InformationTheory.klDiv μ ν = ∫⁻ (x : α), ENNReal.ofReal (InformationTheory.klFun (μ.rnDeriv ν x).toReal) ∂ν
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  (∀ (j : ι), ∃ i, c.Rel i j) →
    ∀ (j : ι),
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inrX K j)
          ((HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K).f j) =
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.inrX K j)
          ((CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) (HomologicalComplex.cylinder.ι₀ K) -
                CategoryTheory.CategoryStruct.id K.cylinder).f
            j)
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- The separable degree equals the degree of any separable contraction, i.e., it is unique.  -/
Polynomial.IsSeparableContraction.degree_eq : ∀ {F : Type u_1} [inst : Field F] (q : ℕ) {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f)
  [hF : ExpChar F q] (g : Polynomial F), Polynomial.IsSeparableContraction q f g → g.natDegree = hf.degree
-- Std.Async.Timer
/-- If:
- `i` is still running this stops `i` without completing any remaining `Async` computations that were created
  through `tick`. Note that if another `Async` computation is binding on any of these it will hang
  forever without further intervention.
- `i` is not yet or not anymore running this is a no-op.
 -/
Std.Async.Interval.stop : Std.Async.Interval → IO Unit
-- Init.SimpLemmas
Nat.le_zero_eq : ∀ (a : ℕ), (a ≤ 0) = (a = 0)
-- Mathlib.Algebra.Ring.Periodic
/-- Lift a periodic function to a function from the quotient group.  -/
Function.Periodic.lift : {α : Type u_1} →
  {β : Type u_2} →
    {f : α → β} → {c : α} → [inst : AddGroup α] → Function.Periodic f c → α ⧸ AddSubgroup.zmultiples c → β
-- Mathlib.Data.Rat.Star
Rat.instStarOrderedRing : StarOrderedRing ℚ
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- The fractional ideals of a domain `R` are ideals of `R` divided by some `a ∈ R`.

More precisely, let `P` be a localization of `R` at some submonoid `S`,
then a fractional ideal `I ⊆ P` is an `R`-submodule of `P`,
such that there is an `a ∈ S` with `a I ⊆ R`.
 -/
FractionalIdeal : {R : Type u_1} →
  [inst : CommRing R] → Submonoid R → (P : Type u_2) → [inst_1 : CommRing P] → [Algebra R P] → Type (max 0 u_2)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.toPrecylinder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
      {A : C} → HomotopicalAlgebra.Cylinder A → HomotopicalAlgebra.Precylinder A
-- Mathlib.Algebra.Algebra.Hom
/-- Turn an algebra homomorphism into the corresponding additive monoid homomorphism.  -/
AlgHom.toAddMonoidHom' : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → A →+ B
-- Mathlib.Algebra.Field.Basic
Field.toGrindField : {K : Type u_1} → [Field K] → Lean.Grind.Field K
-- Mathlib.Algebra.Group.End
Equiv.Perm.val_equivUnitsEnd_apply : ∀ {α : Type u_4} (e : Equiv.Perm α) (a : α), ↑(Equiv.Perm.equivUnitsEnd e) a = e a
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.mk_eq_mk' : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0),
  RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.tendsto_dist_agmSequences_atTop_zero : ∀ {x y : NNReal}, Filter.Tendsto (fun n => dist (x.agmSequences y n).1 (x.agmSequences y n).2) Filter.atTop (nhds 0)
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.continuousOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {s : Set 𝕜} {f f' : 𝕜 → F}, (∀ x ∈ s, HasDerivAt f (f' x) x) → ContinuousOn f s
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_intCast : ∀ {R : Type u_1} {a b : R} [inst : AddCommGroupWithOne R] (n : ℤ), QuadraticAlgebra.C ↑n = ↑n
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_singleL : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rs : ℕ) (rk : α) (rv : β rk)
  (rl rr : Std.DTreeMap.Internal.Impl α β),
  l.Balanced →
    (Std.DTreeMap.Internal.Impl.inner rs rk rv rl rr).Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size rs ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond rs l.size →
        rs > Std.DTreeMap.Internal.delta * l.size →
          rl.size < Std.DTreeMap.Internal.ratio * rr.size →
            (Std.DTreeMap.Internal.Impl.singleL k v l rk rv rl rr).Balanced
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_mem_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, k ∈ (↑m).keysArray → m.contains k = true
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- Two absolute values `v` and `w` are *equivalent* if `v x ≤ v y` precisely when
`w x ≤ w y`.

Note that for real absolute values this condition is equivalent to the existence of a positive
real number `c` such that `v x ^ c = w x` for all `x`. See
`AbsoluteValue.isEquiv_iff_exists_rpow_eq`.  -/
AbsoluteValue.IsEquiv : {R : Type u_1} →
  [inst : Semiring R] →
    {S : Type u_2} → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → AbsoluteValue R S → Prop
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_monomial_same : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (c : R), ((Polynomial.monomial n) c).coeff n = c
-- Mathlib.RingTheory.RingInvo
RingInvo.mk.sizeOf_spec : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : SizeOf R] (toRingEquiv : R ≃+* Rᵐᵒᵖ)
  (involution' : ∀ (x : R), MulOpposite.unop (toRingEquiv.toFun (MulOpposite.unop (toRingEquiv.toFun x))) = x),
  sizeOf { toRingEquiv := toRingEquiv, involution' := involution' } = 1 + sizeOf toRingEquiv
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.mapsTo_Ioo : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  StrictMonoOn f (Set.Icc a b) → Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_diff_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_eq_iff : ∀ {a x : Ordinal.{u}}, x.invVeblen₂ = a ↔ Ordinal.omega0 ^ x = Ordinal.veblen x.invVeblen₁ a
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.IsIntegral.mk : ∀ {X : AlgebraicGeometry.Scheme},
  autoParam (Nonempty ↥X) AlgebraicGeometry.IsIntegral.nonempty._autoParam →
    autoParam (∀ (U : X.Opens) [Nonempty ↥↑U], IsDomain ↑(X.presheaf.obj (Opposite.op U)))
        AlgebraicGeometry.IsIntegral.component_integral._autoParam →
      AlgebraicGeometry.IsIntegral X
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.BorelCantelli.process_zero : ∀ {Ω : Type u_2} {s : ℕ → Set Ω}, MeasureTheory.BorelCantelli.process s 0 = 0
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_graph_snd_inj : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) {x y : E} {x' y' : F},
  (x, x') ∈ f.graph → (y, y') ∈ f.graph → x = y → x' = y'
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- **Alias** of the reverse direction of `EuclideanGeometry.Sphere.isTangentAt_iff_dist_sq_eq_power`.

---

A line through a point on a sphere is tangent if and only if the squared distance
from the external point to the tangent point equals the power of the point.  -/
EuclideanGeometry.Sphere.isTangentAt_of_dist_sq_eq_power : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t p : P} {s : EuclideanGeometry.Sphere P},
  t ∈ s → dist p t ^ 2 = s.power p → s.IsTangentAt t line[ℝ, p, t]
-- Mathlib.Algebra.Lie.LieTheorem
LieModule.exists_nontrivial_weightSpace_of_lieIdeal : ∀ {k : Type u_1} [inst : Field k] {L : Type u_2} [inst_1 : LieRing L] [inst_2 : LieAlgebra k L] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : LieRingModule L V] [inst_6 : LieModule k L V] [CharZero k]
  [Module.Finite k V] [LieModule.IsTriangularizable k L V] (A : LieIdeal k L),
  IsCoatom ↑A →
    ∀ (χ₀ : Module.Dual k ↥A) [Nontrivial ↥(LieModule.weightSpace V ⇑χ₀)], ∃ χ, Nontrivial ↥(LieModule.weightSpace V ⇑χ)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insertIfNew k v).maxKey?.isSome = true
-- Mathlib.Data.Stream.Init
Stream'.take_add : ∀ {α : Type u} (m n : ℕ) (a : Stream' α), Stream'.take (m + n) a = Stream'.take m a ++ Stream'.take n (Stream'.drop m a)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk.inj : ∀ {M : Type u_3} {inst : MulOneClass M} {toSubsemigroup : Subsemigroup M} {one_mem' : 1 ∈ toSubsemigroup.carrier}
  {toSubsemigroup_1 : Subsemigroup M} {one_mem'_1 : 1 ∈ toSubsemigroup_1.carrier},
  { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } =
      { toSubsemigroup := toSubsemigroup_1, one_mem' := one_mem'_1 } →
    toSubsemigroup = toSubsemigroup_1
-- Mathlib.MeasureTheory.Measure.AEDisjoint
Disjoint.aedisjoint : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  Disjoint s t → MeasureTheory.AEDisjoint μ s t
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.lower_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (F : CategoryTheory.Functor (CategoryTheory.MonoOver Y) (CategoryTheory.MonoOver X)),
  (CategoryTheory.toThinSkeleton (CategoryTheory.MonoOver Y)).comp (CategoryTheory.Subobject.lower F) =
    F.comp (CategoryTheory.toThinSkeleton (CategoryTheory.MonoOver X))
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instSMulCommClassSubtypePreLpMemAddSubgroup : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {α : Type u_3} {E : α → Type u_4} {p : ENNReal}
  [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜] [inst_2 : NormedRing 𝕜']
  [inst_3 : (i : α) → Module 𝕜 (E i)] [inst_4 : (i : α) → Module 𝕜' (E i)] [inst_5 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [inst_6 : ∀ (i : α), IsBoundedSMul 𝕜' (E i)] [∀ (i : α), SMulCommClass 𝕜' 𝕜 (E i)], SMulCommClass 𝕜' 𝕜 ↥(lp E p)
-- Mathlib.Data.ENNReal.Basic
ENNReal.iSup_coe_lt_top : ∀ {ι : Sort u_2} {f : ι → NNReal}, ⨆ i, ↑(f i) < ⊤ ↔ BddAbove (Set.range f)
-- Lean.Elab.Do.Control
/-- Elaborate `elabElem` in the lifted stack: install `break`/`continue`/`return`
handlers funnelling into `liftedStack` and set the doBlock result type to
`liftedDoBlockResultType`. Semantically
`MonadControl.liftWith fun runInBase => elabElem (runInBase pure)`. Conts
passed to `elabElem` are implicitly wrapped in `runInBase`, realised later by
`ControlStack.mkBreak`/`mkContinue`/`mkReturn` once the transformer stack `t` is fixed by
aggregating effects across *all* `lift` sites for this lifter.
 -/
Lean.Elab.Do.EffectForwarder.lift : Lean.Elab.Do.EffectForwarder →
  (Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Expr) → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.CategoryTheory.Generator.Abelian
CategoryTheory.Abelian.has_projective_separator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.Limits.HasColimits C] [CategoryTheory.EnoughProjectives C] (G : C),
  CategoryTheory.IsCoseparator G → ∃ G, CategoryTheory.Projective G ∧ CategoryTheory.IsSeparator G
-- Mathlib.NumberTheory.Multiplicity
padicValNat.pow_sub_pow : ∀ {x y p : ℕ} [hp : Fact (Nat.Prime p)],
  Odd p →
    y < x →
      p ∣ x - y → ¬p ∣ x → ∀ {n : ℕ}, n ≠ 0 → padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n
-- Mathlib.Probability.Process.Kolmogorov
/-- Property of being a modification of a stochastic process that satisfies the Kolmogorov
condition (`IsKolmogorovProcess`).  -/
ProbabilityTheory.IsAEKolmogorovProcess : {T : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      [PseudoEMetricSpace T] →
        {mΩ : MeasurableSpace Ω} →
          [PseudoEMetricSpace E] → (T → Ω → E) → MeasureTheory.Measure Ω → ℝ → ℝ → NNReal → Prop
-- Lean.Compiler.IR.CompilerM
Lean.IR.DeclMap : Type
-- Aesop.Rule.Name
Aesop.BuilderName.simp : Aesop.BuilderName
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two functions coincide on a set `s`, then a Taylor series for the first one is as well a
Taylor series for the second one.  -/
HasFTaylorSeriesUpToOn.congr : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → (∀ x ∈ s, f₁ x = f x) → HasFTaylorSeriesUpToOn n f₁ p s
-- Mathlib.Data.Int.Log
Int.log_inv : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b : ℕ) (r : R), Int.log b r⁻¹ = -Int.clog b r
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.id_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : G.Coalgebra),
  (CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.A