mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_appLE : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : X.Opens)
  (e : V ≤ (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U),
  AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U V e =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U)
      (AlgebraicGeometry.Scheme.Hom.appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e)
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_1 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (x : Nat.Partrec.Code) (h_1 : (x : Nat.Partrec.Code) → motive 0 x)
  (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero) (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ)
  (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left) (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match 0, x with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_1 x
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.State : Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {fallback v : β},
      Std.DHashMap.Raw.Const.getD (m.insert k v) a fallback =
        if (k == a) = true then v else Std.DHashMap.Raw.Const.getD m a fallback
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq c = Lean.Meta.Grind.Arith.Cutsat.UnsatProof.diseq c_1) = (c = c_1)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_antiperiod_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
  Function.Periodic f c₁ → Function.Antiperiodic f c₂ → f (c₁ - c₂) = -f 0
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.coe_T_zpow : ∀ (n : ℤ), ↑(ModularGroup.T ^ n) = !![1, n; 0, 1]
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : LawfulBEq α]
  {f : α → β → γ} {k : α} {h' : k ∈ Std.HashMap.map f m}, (Std.HashMap.map f m)[k] = f k m[k]
-- Mathlib.Topology.Connected.LocallyPathConnected
IsOpen.locallyPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X},
  IsOpen U → LocallyPathConnectedSpace ↑U
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).size =
        if Std.DTreeMap.Internal.Impl.contains k t = true then t.size - 1 else t.size
-- Mathlib.SetTheory.ZFC.Basic
/-- Indexed union of a family of ZFC sets. Uses `⋃` notation, scoped under the `ZFSet` namespace.  -/
ZFSet.«term⋃_,_» : Lean.ParserDescr
-- Mathlib.RingTheory.Regular.IsSMulRegular
isSMulRegular_iff_ker_lsmul_eq_bot : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R),
  IsSMulRegular M r ↔ ((LinearMap.lsmul R M) r).ker = ⊥
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Any regular additive Haar measure is invariant under negation in an abelian group.  -/
MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [LocallyCompactSpace G]
  [μ.InnerRegular], μ.IsNegInvariant
-- Lean.Parser.Term
Lean.Parser.Term.clear.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.inl.eq_1 : ∀ (G₀ : Type u_1) (H₀ : Type u_2) [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0],
  MonoidWithZeroHom.inl G₀ H₀ =
    (WithZero.map' (MonoidHom.inl G₀ˣ H₀ˣ)).comp (MonoidWithZeroHom.ofClass WithZero.withZeroUnitsEquiv.symm)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.subset_vanishingIdeal_zeroLocus : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (s : Set A), s ⊆ ↑(ProjectiveSpectrum.vanishingIdeal (ProjectiveSpectrum.zeroLocus 𝒜 s))
-- Mathlib.Tactic.ComputeAsymptotics.Lemmas
Tactic.ComputeAsymptotics.isBigOWith_of_tendsto_top : ∀ {C : ℝ} {f g : ℝ → ℝ} {l : Filter ℝ},
  Filter.Tendsto (fun x => g x / f x) l Filter.atTop → 0 < C → Asymptotics.IsBigOWith C l f g
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- Multiplicative equivalence between multiplicative endomorphisms of a `MulOneClass` `M`
and additive endomorphisms of `Additive M`.  -/
monoidEndToAdditive : (M : Type u_4) → [inst : MulOneClass M] → Monoid.End M ≃* AddMonoid.End (Additive M)
-- Mathlib.Data.Set.Card
Set.one_le_ncard_insert : ∀ {α : Type u_1} (a : α) (s : Set α), autoParam s.Finite Set.one_le_ncard_insert._auto_1 → 1 ≤ (insert a s).ncard
-- Lean.Data.PersistentArray
Lean.PersistentArray.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (root : Lean.PersistentArrayNode α) (tail : Array α) (size : ℕ) (shift : USize)
  (tailOff : ℕ),
  sizeOf { root := root, tail := tail, size := size, shift := shift, tailOff := tailOff } =
    1 + sizeOf root + sizeOf tail + sizeOf size + sizeOf shift + sizeOf tailOff
-- Mathlib.Data.TypeVec
/-- identity of arrow composition  -/
TypeVec.id : {n : ℕ} → {α : TypeVec.{u_1} n} → α.Arrow α
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.instZero : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              (x : Submonoid A) →
                [inst_3 : AddCommMonoid ι] →
                  [inst_4 : DecidableEq ι] → [GradedRing 𝒜] → Zero (HomogeneousLocalization.NumDenSameDeg 𝒜 x)
-- Mathlib.CategoryTheory.Yoneda
/-- The curried version of coyoneda lemma when `C` is small.  -/
CategoryTheory.curriedCoyonedaLemma : {C : Type u₁} →
  [inst : CategoryTheory.SmallCategory C] →
    CategoryTheory.coyoneda.rightOp.comp CategoryTheory.coyoneda ≅ CategoryTheory.evaluation C (Type u₁)
-- Mathlib.Data.Finset.Grade
/-- **Alias** of the reverse direction of `Finset.coe_wcovBy_coe`. -/
WCovBy.finset_coe : ∀ {α : Type u_1} {s t : Finset α}, s ⩿ t → ↑s ⩿ ↑t
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul.injEq : ∀ (a? : Option Lean.Expr) (cs : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)) (a?_1 : Option Lean.Expr)
  (cs_1 : Array (Lean.Expr × ℤ × Lean.Meta.Grind.Arith.Cutsat.EqCnstr)),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul a? cs = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mul a?_1 cs_1) =
    (a? = a?_1 ∧ cs = cs_1)
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.rightInverse_symm : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (e : A ≃⋆+* B), Function.RightInverse ⇑e.symm ⇑e
-- Mathlib.Algebra.Group.Prod
MulHom.snd.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : Mul M] [inst_1 : Mul N], MulHom.snd M N = { toFun := Prod.snd, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_def : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ - ν = sInf {d | μ ≤ d + ν}
-- Mathlib.Analysis.Normed.Group.Defs
ENormedCommMonoid.enorm_eq_zero : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ENormedCommMonoid E] (x : E), ‖x‖ₑ = 0 ↔ x = 1
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.continuousAt_extend_symm' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : E},
  x ∈ (f.extend I).target → ContinuousAt (↑(f.extend I).symm) x
-- Mathlib.Topology.Homotopy.Lifting
/-- The monodromy action of the fundamental group at `x` on the fiber over `x`.  -/
IsCoveringMap.fundamentalGroupMulAction : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {p : E → X} → IsCoveringMap p → (x : X) → MulAction (FundamentalGroup X x) ↑(p ⁻¹' {x})
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_swap_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set (α × β)},
  MeasurableSet (Prod.swap ⁻¹' s) ↔ MeasurableSet s
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorObjImpl_tgt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (X.tensorObjImpl Y).tgt = (X.tgt ⨯ Y.tgt)
-- Mathlib.Topology.Constructions.SumProd
/-- **Alias** of `isOpen_setOfPred_disjoint_nhds_nhds`. -/
isOpen_setOf_disjoint_nhds_nhds : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen {p | Disjoint (nhds p.1) (nhds p.2)}
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.writtenInCharts : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x),
  Set.EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (Prod.fst ∘ ⇑h.equiv) (h.domChart.extend I).target
-- Mathlib.RingTheory.Polynomial.IsIntegral
/-- **Alias** of `IsIntegral.coeff`.

---

[Stacks Tag 00H0](https://stacks.math.columbia.edu/tag/00H0) ((2)) -/
IsIntegral.coeff_of_isFractionRing : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Polynomial S},
  IsIntegral (Polynomial R) p → ∀ (i : ℕ), IsIntegral R (p.coeff i)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_add_div : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → ∀ (c : Ordinal.{u_4}), (b * a + c) / b = a + c / b
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by adding a constant value to both the lower and upper bounds.
 -/
Std.Time.Internal.Bounded.LE.neg : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → Std.Time.Internal.Bounded.LE (-m) (-n)
-- Mathlib.Data.Bundle
/-- The trivial bundle, unlike other bundles, has a canonical projection on the fiber.  -/
Bundle.TotalSpace.trivialSnd : (B : Type u_4) → (F : Type u_5) → Bundle.TotalSpace F (Bundle.Trivial B F) → F
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dKernelSequence.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X X_1 : CategoryTheory.Abelian.SpectralObject C ι),
  X = X_1 →
    ∀ {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ f₁_1 : i₀ ⟶ i₁),
      f₁ = f₁_1 →
        ∀ (f₂ f₂_1 : i₁ ⟶ i₂) (e_f₂ : f₂ = f₂_1) (f₃ f₃_1 : i₂ ⟶ i₃) (e_f₃ : f₃ = f₃_1) (f₄ f₄_1 : i₃ ⟶ i₄),
          f₄ = f₄_1 →
            ∀ (f₅ f₅_1 : i₄ ⟶ i₅),
              f₅ = f₅_1 →
                ∀ (f₂₃ f₂₃_1 : i₁ ⟶ i₃) (e_f₂₃ : f₂₃ = f₂₃_1) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
                  (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1) (n₁ n₁_1 : ℤ) (e_n₁ : n₁ = n₁_1) (n₂ n₂_1 : ℤ) (e_n₂ : n₂ = n₂_1)
                  (n₃ n₃_1 : ℤ) (e_n₃ : n₃ = n₃_1) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) (hn₃ : n₂ + 1 = n₃),
                  X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
                    X_1.dKernelSequence f₁_1 f₂_1 f₃_1 f₄_1 f₅_1 f₂₃_1 ⋯ n₀_1 n₁_1 n₂_1 n₃_1 ⋯ ⋯ ⋯
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.pow_le : ∀ {κ μ : Cardinal.{u}}, Cardinal.aleph0 ≤ κ → μ < Cardinal.aleph0 → κ ^ μ ≤ κ
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.instCStarModuleForall : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {ι : Type u_2} →
        {E : ι → Type u_3} →
          [inst_2 : Fintype ι] →
            [inst_3 : (i : ι) → NormedAddCommGroup (E i)] →
              [inst_4 : (i : ι) → Module ℂ (E i)] →
                [inst_5 : (i : ι) → SMul A (E i)] →
                  [inst_6 : (i : ι) → CStarModule A (E i)] →
                    [StarOrderedRing A] → CStarModule A (WithCStarModule A ((i : ι) → E i))
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Given two disjoint closed sets `s, t` in a Hausdorff σ-compact finite-dimensional manifold,
there exists an infinitely smooth function that is equal to `0` exactly on `s` and to `1`
exactly on `t`. See also `exists_contMDiffMap_zero_one_of_isClosed` for a
slightly weaker version.  -/
exists_contMDiff_zero_iff_one_iff_of_isClosed : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] [T2Space M] {n : ℕ∞} {s t : Set M},
  IsClosed s →
    IsClosed t →
      Disjoint s t →
        ∃ f,
          ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) f ∧
            Set.range f ⊆ Set.Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
-- Lean.Expr
/-- Annotate `e` with `pp.numericTypes := flag`
The delaborator uses `pp` options.
 -/
Lean.Expr.setPPNumericTypes : Lean.Expr → Bool → Lean.Expr
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_mul : ∀ {a b : ISize} (h : System.Platform.numBits = 64), (a * b).toBitVec64 h = a.toBitVec64 h * b.toBitVec64 h
-- Mathlib.Data.Set.Pointwise.Support
mulSupport_comp_inv_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Group α] [inst_1 : MulAction α β] [inst_2 : One γ] (c : α)
  (f : β → γ), (Function.mulSupport fun x => f (c⁻¹ • x)) = c • Function.mulSupport f
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map which sends non-zero elements to
non-zero elements, `j : M →+ M'` is an injective group homomorphism, such that the scalar
multiplications on `M` and `M'` are compatible, then the rank of `M / R` is smaller than or equal to
the rank of `M' / R'`. As a special case, taking `R = R'` it is
`LinearMap.lift_rank_le_of_injective`.  -/
lift_rank_le_of_injective_injective : ∀ {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : Ring R'] [inst_4 : AddCommGroup M'] [inst_5 : Module R' M'] (i : R' → R)
  (j : M →+ M'),
  (∀ (r : R'), i r = 0 → r = 0) →
    Function.Injective ⇑j →
      (∀ (r : R') (m : M), j (i r • m) = r • j m) →
        Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : α → M},
  (φ.iff ψ).Realize v ↔ (φ.Realize v ↔ ψ.Realize v)
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.compare_def : compare = compareLex (compareOn fun x => x.date) (compareOn fun x => x.time)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type (max w v₁))) (X : C)
  (R : F.CorepresentableBy X),
  (CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso F X) R =
    CategoryTheory.NatIso.ofComponents (fun X_1 => equivEquivIso (Equiv.ulift.trans R.homEquiv)) ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountablyGenerated.mk : ∀ {α : Type u_3} [m : MeasurableSpace α],
  (∃ b, b.Countable ∧ m = MeasurableSpace.generateFrom b) → MeasurableSpace.CountablyGenerated α
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Post-composition by a uniform embedding is
a uniform embedding for the uniform structures of uniform convergence.

More precisely, if `f : γ → β` is a uniform embedding,
then `(f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)` is a uniform embedding.  -/
UniformFun.postcomp_isUniformEmbedding : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] [inst_1 : UniformSpace γ] {f : γ → β},
  IsUniformEmbedding f → IsUniformEmbedding (⇑UniformFun.ofFun ∘ (fun x => f ∘ x) ∘ ⇑UniformFun.toFun)
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_rcc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = min (hi + 1) xs.size - lo
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.neZero_length : ∀ {n : ℕ} [NeZero n] (c : OrderedFinpartition n), NeZero c.length
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.indexRealUnits_mul_eq : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  NumberField.IsCMField.indexRealUnits K * (NumberField.IsCMField.unitsMulComplexConjInv K).range.index = 2
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.homFamily_arrow_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y)
  (hf : P f), P.homFamily ⟨CategoryTheory.Arrow.mk f, hf⟩ = f
-- Mathlib.Data.List.Perm.Basic
List.Perm.subset_congr_left : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁.Perm l₂ → (l₁ ⊆ l₃ ↔ l₂ ⊆ l₃)
-- Mathlib.Analysis.Convex.Between
sbtw_zero_one_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] {x : R}, Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1
-- Lean.Meta.Closure
Lean.Meta.Closure.State.nextExprIdx : Lean.Meta.Closure.State → ℕ
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instHasHomologyOppositeObjSymmOpFunctorOp : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i],
  ((HomologicalComplex.opFunctor V c).obj (Opposite.op K)).HasHomology i
-- Mathlib.ModelTheory.DirectLimit
/-- Raises a family of elements in the `Σ`-type to the same level along the embeddings.  -/
FirstOrder.Language.DirectLimit.unify : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      {G : ι → Type w} →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            {α : Type u_1} →
              (x : α → FirstOrder.Language.Structure.Sigma f) →
                (i : ι) → i ∈ upperBounds (Set.range (Sigma.fst ∘ x)) → α → G i
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapCyclesIso_hom_naturality : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasLeftHomology]
  [inst_6 : S₂.HasLeftHomology] [inst_7 : F.PreservesLeftHomologyOf S₁] [inst_8 : F.PreservesLeftHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ))
      (S₂.mapCyclesIso F).hom =
    CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).hom (F.map (CategoryTheory.ShortComplex.cyclesMap φ))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_le_minKey!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.erase k ≠ ∅ → (cmp t.minKey! (t.erase k).minKey!).isLE = true
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
UniformContinuousOn.comp_tendstoLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [inst_2 : UniformSpace γ] {g : β → γ} {t : Set β},
  UniformContinuousOn g t →
    TendstoLocallyUniformlyOn F f p s →
      Set.MapsTo f s t →
        (∀ᶠ (n : ι) in p, Set.MapsTo (F n) s t) → TendstoLocallyUniformlyOn (fun x => g ∘ F x) (g ∘ f) p s
-- Mathlib.RingTheory.Radical.Basic
/-- The finset of prime factors of `x` is empty if and only if `x` is a unit.
The converse is true without the nonzero assumption, see `primeFactors_of_isUnit`.
 -/
UniqueFactorizationMonoid.primeFactors_eq_empty_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, a ≠ 0 → (UniqueFactorizationMonoid.primeFactors a = ∅ ↔ IsUnit a)
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
/-- The `shiftIso` field of the induced shift sequence.  -/
CategoryTheory.Functor.ShiftSequence.induced.shiftIso : {C : Type u_1} →
  {D : Type u_2} →
    {A : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} A] →
            (L : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor C A) →
                (M : Type u_4) →
                  [inst_3 : AddMonoid M] →
                    [inst_4 : CategoryTheory.HasShift C M] →
                      [inst_5 : G.ShiftSequence M] →
                        (F' : M → CategoryTheory.Functor D A) →
                          ((m : M) → L.comp (F' m) ≅ G.shift m) →
                            [((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full] →
                              [((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] →
                                [inst_8 : CategoryTheory.HasShift D M] →
                                  [L.CommShift M] →
                                    (n a a' : M) → n + a = a' → ((CategoryTheory.shiftFunctor D n).comp (F' a) ≅ F' a')
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivAt.add` -/
HasFDerivAt.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → HasFDerivAt g g' x → HasFDerivAt (fun i => f i + g i) (f' + g') x
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.linkTarget.notUrlEnd : Lean.Parser.ParserFn