mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
/-- Rescaling a satellite configuration in a vector space, to put the basepoint at `0` and the base
radius at `1`.  -/
Besicovitch.SatelliteConfig.centerAndRescale : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [NormedSpace ℝ E] → {N : ℕ} → {τ : ℝ} → Besicovitch.SatelliteConfig E N τ → Besicovitch.SatelliteConfig E N τ
-- Mathlib.Data.List.Map2
List.zipRight_eq_zipRight' : ∀ {α : Type u} {β : Type v} (as : List α) (bs : List β), as.zipRight bs = (as.zipRight' bs).1
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.nil : Lean.IR.FnBody
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.functorialityCounit'_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) (c : CategoryTheory.Limits.Cone K),
  ((adj.functorialityCounit' K).app c).hom = adj.counit.app c.pt
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The underlying space of the completion.  -/
AbstractCompletion.space : {α : Type u} → [inst : UniformSpace α] → AbstractCompletion.{v, u} α → Type v
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.not_isIntegralHom : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [Nonempty ↥S] [Nonempty n],
  ¬AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules : ∀ {X : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.Modules.toPresheafOfModules X).Faithful
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀_smul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} {R : Type u_5} [inst_3 : Ring R]
  [inst_4 : CategoryTheory.Preadditive C] [inst_5 : CategoryTheory.Linear R C] (m₀ : M) (hm₀ : m₀ = 0) (r : R)
  {f : X ⟶ Y}, CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (r • f) = r • CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurveAt.continuousAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ},
  IsIntegralCurveAt γ v t₀ → ContinuousAt γ t₀
-- Mathlib.Order.Cover
wcovBy_iff_eq_or_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b ↔ a = b ∨ a ⋖ b
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.coe_pow : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] (x : ↥H)
  (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Init.Data.Int.Cooper
/-- Given a solution `x` to a divisibility constraint `a ∣ b * x + c`,
then `x % d` is another solution as long as `(a / gcd a b) | d`.

See `dvd_emod_add_of_dvd_add` for the specialization with `b = 1`.
 -/
Int.dvd_mul_emod_add_of_dvd_mul_add : ∀ {a b c d x : ℤ}, a ∣ b * x + c → a / ↑(a.gcd b) ∣ d → a ∣ b * (x % d) + c
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.inv_zero : ∀ {α : Type u_1} [inst : GroupWithZero α], 0⁻¹ = 0
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
setIntegral_withDensity_eq_setIntegral_smul₀ : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {f : X → NNReal} {s : Set X},
  AEMeasurable f (μ.restrict s) →
    ∀ (g : X → E), MeasurableSet s → (∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ
-- Std.Data.HashSet.Lemmas
Std.HashSet.insert_eq_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {a : α}, insert a m = m.insert a
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.IterM.step_takeWhile.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : true = true → motive true) (h_2 : true = false → motive false),
  (match hP : true with
    | true => h_1 hP
    | false => h_2 hP) =
    h_1 ⋯
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- `x` is a conjugate root of `0` if and only if `x = 0`.
 -/
isConjRoot_zero_iff_eq_zero : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [IsDomain S] {x : S},
  IsConjRoot K 0 x ↔ x = 0
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `findGt`.  -/
Ordnode.findGtAux : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → α → α
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map₂_apply_tmul : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12}
  {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid N₂] [inst_7 : AddCommMonoid M₃] [inst_8 : AddCommMonoid N₃]
  [inst_9 : Module R M] [inst_10 : Module R N] [inst_11 : Module R₂ M₂] [inst_12 : Module R₂ N₂]
  [inst_13 : Module R₃ M₃] [inst_14 : Module R₃ N₃] (f : M →ₛₗ[σ₁₃] M₂ →ₛₗ[σ₂₃] M₃) (g : N →ₛₗ[σ₁₃] N₂ →ₛₗ[σ₂₃] N₃)
  (m : M) (n : N), (TensorProduct.map₂ f g) (m ⊗ₜ[R] n) = TensorProduct.map (f m) (g n)
-- Mathlib.LinearAlgebra.LinearPMap
/-- The graph of the inverse generates a `LinearPMap`.  -/
LinearPMap.mem_inverse_graph_snd_eq_zero : ∀ {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},
  f.toFun.ker = ⊥ → ∀ x ∈ Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph, x.1 = 0 → x.2 = 0
-- Mathlib.Algebra.Order.Module.Pointwise
bddAbove_smul_iff_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β]
  {s : Set β} {a : α}, a < 0 → (BddAbove (a • s) ↔ BddBelow s)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MonotoneOn.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [AddRightMono α], MonotoneOn f s → ∀ (a : α), MonotoneOn (fun x => f x + a) s
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Integer powers of meromorphic functions in normal form are in normal form.
 -/
MeromorphicNFOn.zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {n : ℤ} {U : Set 𝕜},
  MeromorphicNFOn f U → MeromorphicNFOn (f ^ n) U
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.continuousWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F]
  [ContinuousSMul 𝕜 F], DifferentiableWithinAt 𝕜 f s x → ContinuousWithinAt f s x
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.finsetProd_subset_finsetProd`.

---

An n-ary version of `Set.mul_subset_mul`.  -/
Set.finset_prod_subset_finset_prod : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α),
  (∀ i ∈ t, f₁ i ⊆ f₂ i) → ∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, f₂ i
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.wideSpan_map : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C)
  (arrows : (j : J) → B ⟶ objs j) {X Y : CategoryTheory.Limits.WidePushoutShape J} (f : X ⟶ Y),
  (CategoryTheory.Limits.WidePushoutShape.wideSpan B objs arrows).map f =
    CategoryTheory.Limits.WidePushoutShape.Hom.casesOn (motive := fun a a_1 x =>
      X = a → Y = a_1 → f ≍ x → (Option.casesOn X B objs ⟶ Option.casesOn Y B objs)) f
      (fun X_1 h =>
        Eq.ndrec (motive := fun X_2 =>
          Y = X_2 →
            f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.id X_2 → (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
          (fun h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : X ⟶ Y) →
                f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.id X →
                  (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
              (fun f h => CategoryTheory.CategoryStruct.id (Option.casesOn X B objs)) ⋯ f)
          h)
      (fun j h =>
        Eq.ndrec (motive := fun {X} =>
          (f : X ⟶ Y) →
            Y = some j →
              f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.init j →
                (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : none ⟶ Y) →
                f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.init j →
                  (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
              (fun f h => arrows j) ⋯ f)
          ⋯ f)
      ⋯ ⋯ ⋯
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `FunLike.coe_sum`. -/
ProbabilityTheory.Kernel.coe_finset_sum : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Lean.Meta.HaveTelescope
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.mk.sizeOf_spec : ∀ (expr exprType exprInit exprResult proof : Lean.Expr) (modified : Bool),
  sizeOf
      { expr := expr, exprType := exprType, exprInit := exprInit, exprResult := exprResult, proof := proof,
        modified := modified } =
    1 + sizeOf expr + sizeOf exprType + sizeOf exprInit + sizeOf exprResult + sizeOf proof + sizeOf modified
-- Init.Data.Array.Lemmas
Array.mem_dite_empty_left : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {xs : ¬p → Array α},
  (x ∈ if h : p then #[] else xs h) ↔ ∃ (h : ¬p), x ∈ xs h
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.HasSubobjectClassifier.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  Nonempty (CategoryTheory.Subobject.Classifier C) → CategoryTheory.HasSubobjectClassifier C
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instAdd : {R : Type u_1} → {a b : R} → [Add R] → Add (QuadraticAlgebra R a b)
-- Mathlib.Algebra.Field.ZMod
_private.Mathlib.Algebra.Field.ZMod.0.ZMod.mul_inv_cancel_aux : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (a : ZMod p), a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.Algebra.Ring.Commute
Commute.mul_self_eq_mul_self_iff : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] [NoZeroDivisors R] {a b : R},
  Commute a b → (a * a = b * b ↔ a = b ∨ a = -b)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instMax : {α : Type u_1} → [inst : LE α] → Max (UpperSet α)
-- Init.Data.BitVec.Lemmas
BitVec.lt_of_msb_false_of_msb_true : ∀ {w : ℕ} {x y : BitVec w}, x.msb = false → y.msb = true → x < y
-- Mathlib.Algebra.Order.Group.Abs
sub_le_of_abs_sub_le_right : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b c : G},
  |a - b| ≤ c → a - c ≤ b
-- Mathlib.Analysis.Analytic.ChangeOrigin
ContinuousMultilinearMap.curryFinFinset.congr_simp : ∀ (𝕜 : Type u) (G : Type wG) (G' : Type wG') [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k l n : ℕ}
  {s s_1 : Finset (Fin n)} (e_s : s = s_1) (hk : s.card = k) (hl : sᶜ.card = l),
  ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl = ContinuousMultilinearMap.curryFinFinset 𝕜 G G' ⋯ ⋯
-- Mathlib.Data.Fintype.Option
/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`.  -/
Fintype.induction_empty_option : ∀ {P : (α : Type u) → [Fintype α] → Prop},
  (∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β) →
    P PEmpty.{u + 1} →
      (∀ (α : Type u) [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type u) [h_fintype : Fintype α], P α
-- Mathlib.Topology.Separation.Hausdorff
Function.LeftInverse.isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space X] {f : X → Y}
  {g : Y → X}, Function.LeftInverse f g → Continuous f → Continuous g → Topology.IsClosedEmbedding g
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.ofReal_condCDF_ae_eq : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (r : ℚ),
  (fun a => ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) ↑r)) =ᵐ[ρ.fst] ProbabilityTheory.preCDF ρ r
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Precomposition with a continuous map is a continuous linear map from bounded continuous
functions to bounded continuous functions.  -/
BoundedContinuousFunction.compContinuousCLM : {α : Type u} →
  (β : Type v) →
    {γ : Type w} →
      [inst : TopologicalSpace α] →
        [inst_1 : SeminormedAddCommGroup β] →
          (𝕜 : Type u_2) →
            [inst_2 : TopologicalSpace γ] →
              [inst_3 : NormedField 𝕜] →
                [inst_4 : NormedSpace 𝕜 β] → C(γ, α) → BoundedContinuousFunction α β →L[𝕜] BoundedContinuousFunction γ β
-- Mathlib.Data.Nat.Prime.Defs
Nat.not_prime_iff_minFac_lt : ∀ {n : ℕ}, 2 ≤ n → (¬Nat.Prime n ↔ n.minFac < n)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_X_pow : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) {n : ℕ},
  (Polynomial.aeval x) (Polynomial.X ^ n) = x ^ n
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- If `K` is the fraction field of a discrete valuation ring `R`, any element `x` of `K` can be
expressed as `u • (algebraMap R K ϖ) ^ n` for some `u : Rˣ` and `n : ℤ`.
 -/
IsDiscreteValuationRing.exists_units_eq_smul_zpow_of_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [inst_3 : Field K]
  [inst_4 : Algebra R K] [IsFractionRing R K] {ϖ : R},
  Irreducible ϖ → ∀ {x : K}, x ≠ 0 → ∃ n u, x = u • (algebraMap R K) ϖ ^ n
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_div_sub_hasFPowerSeriesOnBall_zero : ∀ {z : ℂ},
  z ≠ 0 →
    HasFPowerSeriesOnBall (fun x => 1 / (z - x)) (FormalMultilinearSeries.ofScalars ℂ fun n => (z ^ (n + 1))⁻¹) 0 ‖z‖ₑ
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.hom_inv_associator : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] {M N K : QuadraticModuleCat R},
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv =
    (M.form.tensorAssoc N.form K.form).symm.toIsometry
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x`, `1 x = 1`, and `(f ^ n) x = f x ^ n`
is a commutative monoid if `β` is a commutative monoid.  -/
FunLike.commMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : CommMonoid β] → [IsOneApply F α β] → [IsMulApply F α β] → [IsPowApply ℕ F α β] → CommMonoid F
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_eq_add_of_sub_eq_sub : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {b d : α},
  IsAddUnit b → IsAddUnit d → ∀ (a c : α), a - b = c - d → a + d = c + b
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given an `R`-algebra `S`, the `ℤ`-linear representation associated to the natural action of
`S ≃ₐ[R] S` on `S`.  -/
Rep.ofAlgebraAut : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Rep.{u_2, 0, u_2} ℤ (S ≃ₐ[R] S)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullback_comp_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : C} (f : X ⟶ Y)
  {Z : CategoryTheory.Functor (CategoryTheory.Sheaf (J.over Y) A) (CategoryTheory.Sheaf (J.over X) A)}
  (h : J.overMapPullback A f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A f (CategoryTheory.CategoryStruct.id Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f))
        (CategoryTheory.CategoryStruct.comp (J.overMapPullback A f).leftUnitor.hom h)) =
    CategoryTheory.CategoryStruct.comp (J.overMapPullbackCongr A ⋯).hom h
-- Mathlib.Order.Atoms
IsAtom.le_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a x : α}, IsAtom a → (x ≤ a ↔ x = ⊥ ∨ x = a)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β} {f : β → β}, (t.modify k f).getD k fallback = (Option.map f t[k]?).getD fallback
-- Aesop.Tree.TreeM
Aesop.TreeM.instMonadStateOfTree : MonadStateOf Aesop.Tree Aesop.TreeM
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_eq_zero_iff_sin_eq : ∀ {z : ℂ}, Complex.cos z = 0 ↔ Complex.sin z = 1 ∨ Complex.sin z = -1
-- Mathlib.GroupTheory.Nilpotent
_private.Mathlib.GroupTheory.Nilpotent.0.AddSubgroup.comap_center_subst : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ : AddSubgroup G} [inst_1 : H₁.Normal] [inst_2 : H₂.Normal],
  H₁ = H₂ →
    AddSubgroup.comap (QuotientAddGroup.mk' H₁) (AddSubgroup.center (G ⧸ H₁)) =
      AddSubgroup.comap (QuotientAddGroup.mk' H₂) (AddSubgroup.center (G ⧸ H₂))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km fallback : α}, Std.Internal.List.maxKey? l = some km → Std.Internal.List.getKeyD km l fallback = km
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_singleton_le : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A}
  {a : A}, a ∈ S → R[a] ≤ S
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.equivOfComm_symm_apply : ∀ {H : Type u_1} [inst : CommGroup H] (a : Abelianization H),
  Abelianization.equivOfComm.symm a = (Abelianization.lift (MonoidHom.id H)) a
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) (q : ℚ), MeasureTheory.Integrable (fun t => ⨅ r, f (a, t) ↑r) (ν a)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocTree : Type
-- Mathlib.Data.Nat.Prime.Defs
_private.Mathlib.Data.Nat.Prime.Defs.0.Nat.minFacProp.eq_1 : ∀ (n k : ℕ), Nat.minFacProp✝ n k = (2 ≤ k ∧ k ∣ n ∧ ∀ (m : ℕ), 2 ≤ m → m ∣ n → k ≤ m)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The real mixed space `ℝ^r₁ × (ℝ × ℝ)^r₂` with `(r₁, r₂)` the signature of `K`.
 -/
NumberField.mixedEmbedding.realMixedSpace : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.Order.SuccPred.WithBot
WithBot.succ_eq_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] (a : WithBot α),
  ↑a.succ = Order.succ a
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.unfold : Array Lean.Name → Bool → Aesop.Script.TacticBuilder
-- Mathlib.Data.Set.Lattice
Set.iInter_congr : ∀ {α : Type u_1} {ι : Sort u_5} {s t : ι → Set α}, (∀ (i : ι), s i = t i) → ⋂ i, s i = ⋂ i, t i
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.isEquivalence_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G) [F.IsEquivalence], G.IsEquivalence
-- Mathlib.Logic.Nontrivial.Basic
Option.nontrivial : ∀ {α : Type u_1} [Nonempty α], Nontrivial (Option α)
-- Init.Grind.Offset
Lean.Grind.Nat.le_offset : ∀ (a k : ℕ), k ≤ a + k
-- Lean.Data.Lsp.Internal
/-- Creates a `RefInfo.Location`.  -/
Lean.Lsp.RefInfo.Location.mk : Lean.Lsp.Range → Option String → Lean.Lsp.RefInfo.Location
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toEquiv : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → (P₁ ≃ᵃ[k] P₂) → P₁ ≃ P₂
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  (U : ↑X.affineOpens),
  (I.comap f).ideal U =
    Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appIso f ↑U).inv)
      (I.ideal ⟨(AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ↑U, ⋯⟩)
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Init.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Lean.Meta.Basic
Lean.Meta.instInhabitedExprParamInfo.default : Lean.Meta.ExprParamInfo
-- Mathlib.Algebra.Category.Grp.Zero
AddGrpCat.isZero_of_subsingleton : ∀ (G : AddGrpCat) [Subsingleton ↑G], CategoryTheory.Limits.IsZero G
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_minKey?_of_isSome_minKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).minKey?.isSome = true → t.minKey?.isSome = true
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The product of `f` over `insert a s` is the same as
the product over `s`, as long as `f a = 1`.  -/
Finset.prod_insert_one : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  f a = 1 → ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsMarkovKernel.swapLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.IsMarkovKernel κ.swapLeft
-- Mathlib.NumberTheory.PellMatiyasevic
/-- The Pell `x` sequence, considered as an integer sequence.  -/
Pell.xz : {a : ℕ} → 1 < a → ℕ → ℤ
-- Mathlib.Tactic.Ring.Basic
/-- The data used by `ring`-like tactics to normalize constant coefficients of natural number
expressions.  -/
Mathlib.Tactic.Ring.rcℕ : Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ
-- Init.Data.Nat.Lemmas
Nat.decidableForallFin : {n : ℕ} → (P : Fin n → Prop) → [DecidablePred P] → Decidable (∀ (i : Fin n), P i)