mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- Variant of `UniqueFactorizationMonoid.count_normalizedFactors_eq` for associated Ideals.  -/
Ideal.count_associates_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {a a₀ x : R} {n : ℕ},
  Prime x →
    ¬x ∣ a → a₀ = x ^ n * a → (Associates.mk (Ideal.span {x})).count (Associates.mk (Ideal.span {a₀})).factors = n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : (a : α) → β a → Bool} {k : α}, k ∈ Std.DHashMap.filter f m → k ∈ m
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).get? k' = if h : cmp k k' = Ordering.eq then cast ⋯ (f (t.get? k)) else t.get? k'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_diff_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false →
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.diff m₂ ⋯) k fallback =
          Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
-- Mathlib.Data.EReal.Basic
/-- Induct on two `EReal`s by performing case splits on the sign of one whenever the other is
infinite. This version eliminates some cases by assuming that the relation is symmetric.  -/
EReal.induction₂_symm : ∀ {P : EReal → EReal → Prop},
  (∀ {x y : EReal}, P x y → P y x) →
    P ⊤ ⊤ →
      (∀ (x : ℝ), 0 < x → P ⊤ ↑x) →
        P ⊤ 0 →
          (∀ x < 0, P ⊤ ↑x) →
            P ⊤ ⊥ →
              (∀ (x : ℝ), 0 < x → P ↑x ⊥) →
                (∀ (x y : ℝ), P ↑x ↑y) → P 0 ⊥ → (∀ x < 0, P ↑x ⊥) → P ⊥ ⊥ → ∀ (x y : EReal), P x y
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.pushout.associator_naturality_left_condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {A B X Y Z W : C} {f : A ⟶ B} {g : X ⟶ Y}
  {h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z W ⟶ X} {Z_1 : C}
  (h_1 :
    CategoryTheory.Limits.pushout (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) W)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator B Z W).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B h)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g))
            h_1))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A Z W).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp h g))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g))
          h_1))
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider differentiable maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is differentiable.

We give here a version of this statement on a set.  -/
MDifferentiableOn.clm_bundle_apply₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} {M : Type u_6}
  [inst : NontriviallyNormedField 𝕜] {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8}
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_9} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)] {EB : Type u_10}
  [inst_19 : NormedAddCommGroup EB] [inst_20 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_21 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_22 : TopologicalSpace B] [inst_23 : ChartedSpace HB B] {EM : Type u_12}
  [inst_24 : NormedAddCommGroup EM] [inst_25 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_26 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_27 : TopologicalSpace M] [inst_28 : ChartedSpace HM M]
  [inst_29 : FiberBundle F₁ E₁] [inst_30 : VectorBundle 𝕜 F₁ E₁] [inst_31 : FiberBundle F₂ E₂]
  [inst_32 : VectorBundle 𝕜 F₂ E₂] [inst_33 : FiberBundle F₃ E₃] [inst_34 : VectorBundle 𝕜 F₃ E₃] {b : M → B}, ⋯
-- Init.Data.List.Erase
List.erase_eq_eraseIdx : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (a : α),
  l.erase a =
    match List.idxOf? a l with
    | none => l
    | some i => l.eraseIdx i
-- Init.Data.Bool
Bool.or_eq_true_iff : ∀ {x y : Bool}, (x || y) = true ↔ x = true ∨ y = true
-- Mathlib.Algebra.Group.Action.End
Function.End.mul_def : ∀ {α : Type u_5} (f g : Function.End α), f * g = f ∘ g
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_comp_self : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ⇑e.symm ∘ ⇑e = id
-- Aesop.Forward.Match.Types
Aesop.CompleteMatch.mk.inj : ∀ {clusterMatches clusterMatches_1 : Array Aesop.Match},
  { clusterMatches := clusterMatches } = { clusterMatches := clusterMatches_1 } → clusterMatches = clusterMatches_1
-- Std.Time.Date.ValidDate
/-- Represents a valid date for a given year, considering whether it is a leap year. Example: `(2, 29)`
is valid only if `leap` is `true`.
 -/
Std.Time.ValidDate : Bool → Type
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.ext : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] ⦃f g : IncidenceAlgebra 𝕜 α⦄,
  (∀ (a b : α), a ≤ b → f a b = g a b) → f = g
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_eq_left_inv : ∀ {α : Type u} [inst : Monoid α] {a b : α} [inst_1 : Invertible a], b * a = 1 → ⅟a = b
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.OplaxFunctor B CategoryTheory.Cat}
  (η : CategoryTheory.Oplax.StrongTrans F G) {a b : B} {a' : CategoryTheory.Cat} {f g : a ⟶ b} (β : f ⟶ g)
  (h : G.obj b ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp (h.toFunctor.map ((η.app b).toFunctor.map ((F.map₂ β).toNatTrans.app X)))
      (h.toFunctor.map ((η.naturality g).hom.toNatTrans.app X)) =
    CategoryTheory.CategoryStruct.comp (h.toFunctor.map ((η.naturality f).hom.toNatTrans.app X))
      (h.toFunctor.map ((G.map₂ β).toNatTrans.app ((η.app a).toFunctor.obj X)))
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Turn a monoid object in the opposite category into a comonoid object.
 -/
CategoryTheory.Comon.MonOpOpToComonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Mon Cᵒᵖ → CategoryTheory.Comon C
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_min?_of_isSome_min?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).min?.isSome = true → t.min?.isSome = true
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_tmul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] [inst_13 : AddCommMonoid Q]
  [inst_14 : Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N),
  (TensorProduct.AlgebraTensorModule.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
-- Init.Data.String.Lemmas.Pattern.Find.String
String.contains_slice_iff : ∀ {t : String.Slice} {s : String}, s.contains t = true ↔ t.copy.toList <:+: s.toList
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_inv : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R]
  (f : R → R) (a : A),
  (∀ x ∈ spectrum R a, f x ≠ 0) →
    autoParam (ContinuousOn f (spectrum R a)) cfc_inv._auto_1 →
      autoParam (p a) cfc_inv._auto_3 → cfc (fun x => (f x)⁻¹) a = Ring.inverse (cfc f a)
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_le_encard_iff_encard_sdiff_le_encard_sdiff`. -/
Set.encard_le_encard_iff_encard_diff_le_encard_diff : ∀ {α : Type u_1} {s t : Set α}, (s ∩ t).Finite → (s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.TreeMap.ofList l cmp).getKey? k = none
-- Mathlib.Data.Set.Sups
Set.infs_subset_iff : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t u : Set α}, s ⊼ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a ⊓ b ∈ u
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.image_symm_eq_preimage : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (S : Set B), ⇑e.symm '' S = ⇑e ⁻¹' S
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instInhabited : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Inhabited (DoubleCentralizer 𝕜 A)
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofNat' : ∀ {n : ℕ}, n < UInt8.size → (UInt8.ofNat n).toUSize = USize.ofNat n
-- Mathlib.Analysis.Fourier.ZMod
/-- The discrete Fourier transform agrees with the general one (assuming the target space is a complete
normed space).
 -/
ZMod.dft_eq_fourier : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℂ E] [CompleteSpace E]
  (Φ : ZMod N → E) (k : ZMod N), ZMod.dft Φ k = Fourier.fourierIntegral ZMod.toCircle MeasureTheory.Measure.count Φ k
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.produces_reverse : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)},
  g.reverse.Produces u.reverse v.reverse ↔ g.Produces u v
-- Mathlib.Data.Sym.Sym2
/-- Mapping an unordered pair to a finite set produces a finset of size `1` if the pair is on the
diagonal, else of size `2` if the pair is off the diagonal.  -/
Sym2.card_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (z : Sym2 α), z.toFinset.card = if z.IsDiag then 1 else 2
-- Mathlib.Algebra.Category.BoolRing
/-- The equivalence between Boolean rings and Boolean algebras. This is actually an isomorphism.  -/
boolRingCatEquivBoolAlg : BoolRing ≌ BoolAlg
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isSingular_aleph_iff : ∀ {o : Ordinal.{u_1}}, (Cardinal.aleph o).IsSingular ↔ Order.IsSuccLimit o ∧ o.cof < Cardinal.aleph o
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.vadd_asymptoticNhds : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] (u v : V),
  u +ᵥ AffineSpace.asymptoticNhds k P v = AffineSpace.asymptoticNhds k P v
-- Init.Data.Fin.Lemmas
Fin.div_val : ∀ {n : ℕ} (a b : Fin n), ↑(a / b) = ↑a / ↑b
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.inner_eq_star_dotProduct : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype ι] (x y : EuclideanSpace 𝕜 ι),
  inner 𝕜 x y = y.ofLp ⬝ᵥ star x.ofLp
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instSetLike.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M],
  SubMulAction.instSetLike = { coe := SubMulAction.carrier, coe_injective := ⋯ }
-- Mathlib.AlgebraicGeometry.ResidueField
/-- The canonical map `Spec κ(x) ⟶ X`.  -/
AlgebraicGeometry.Scheme.fromSpecResidueField : (X : AlgebraicGeometry.Scheme) → (x : ↥X) → AlgebraicGeometry.Spec (X.residueField x) ⟶ X
-- Mathlib.Order.CompleteLatticeIntervals
subset_sInf_def : ∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : InfSet α] [inst_2 : Inhabited ↑s],
  sInf = fun t =>
    if ht : t.Nonempty ∧ BddBelow t ∧ sInf (Subtype.val '' t) ∈ s then ⟨sInf (Subtype.val '' t), ⋯⟩ else default
-- Mathlib.SetTheory.Ordinal.Veblen
_private.Mathlib.SetTheory.Ordinal.Veblen.0.Ordinal.cmp_veblenWith.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.lt)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.eq => h_1 ()
    | Ordering.lt => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {fallback : α},
  (t.insert k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.support_truncFinset_subset : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} (p : MvPowerSeries σ R),
  ((MvPowerSeries.truncFinset R s) p).support ⊆ s
-- Mathlib.Order.Lattice
inf_le_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c d : α}, b ≤ a → d ≤ c → b ⊓ d ≤ a ⊓ c
-- Mathlib.Topology.Compactness.SigmaCompact
/-- Compact sets are σ-compact.  -/
IsCompact.isSigmaCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → IsSigmaCompact s
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingProd_cons_cons' : ∀ {G : Type u_7} [inst : One G] [inst_1 : Mul G] [inst_2 : Inv G] (a b : G) (l : List G),
  (a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.natIso_inv : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {q₁ q₂ : CategoryTheory.Functor ((i : I) × C i) D}
  (h : (i : I) → (CategoryTheory.Sigma.incl i).comp q₁ ≅ (CategoryTheory.Sigma.incl i).comp q₂),
  (CategoryTheory.Sigma.natIso h).inv = CategoryTheory.Sigma.natTrans fun i => (h i).inv
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  [AlgebraicGeometry.Flat iX],
  AlgebraicGeometry.IsAffineOpen US →
    IsCompact ↑UT →
      IsCompact ↑UX →
        (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f US UT hUST)).Flat →
          CategoryTheory.Mono (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.of_insert : ∀ {𝕜 : 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} {f' : E →L[𝕜] F} {x : E} {s : Set E} {y : E},
  HasFDerivWithinAt f f' (insert y s) x → HasFDerivWithinAt f f' s x
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  W.IsStableUnderTransfiniteCompositionOfShape J ↔ W.transfiniteCompositionsOfShape J ≤ W
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.snd_comp_prod : ∀ {R : Type u_1} {S : Type u_3} {T : Type u_5} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T),
  (NonUnitalRingHom.snd S T).comp (f.prod g) = g
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Alias** of `isCompact_setOfPred_finiteMeasure_le_of_isCompact`.

---

The set of finite measures of mass at most `C` supported on a given compact set `K` is
compact.  -/
isCompact_setOf_finiteMeasure_le_of_isCompact : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  (C : NNReal) {K : Set E}, IsCompact K → IsCompact {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_sdiff : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V} (v : V), (G₁ \ G₂).neighborSet v = G₁.neighborSet v \ G₂.neighborSet v
-- Mathlib.Algebra.Algebra.Basic
Algebra.algebraMapSubmonoid_self : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R), Algebra.algebraMapSubmonoid R M = M
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.isFiniteMeasure_toFiniteAux : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ],
  MeasureTheory.IsFiniteMeasure μ.toFiniteAux
-- Lean.DocString.Extension
Lean.instInhabitedVersoDocString.default : Lean.VersoDocString
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (F : CategoryTheory.Limits.MonoFactorisation f) →
          CategoryTheory.Limits.IsImage F → CategoryTheory.Limits.ImageFactorisation f
-- Init.Data.List.Basic
List.head_cons : ∀ {α : Type u} {a : α} {l : List α} {h : a :: l ≠ []}, (a :: l).head h = a
-- Std.Data.DHashMap.Basic
Std.DHashMap.instForInSigmaOfMonad : {α : Type u} →
  {β : α → Type v} →
    {m : Type w → Type w'} →
      [Monad m] → [inst : BEq α] → [inst_1 : Hashable α] → ForIn m (Std.DHashMap α β) ((a : α) × β a)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Geometric progressions of length three are reflected under `2`-Freiman homomorphisms.  -/
ThreeGPFree.of_image : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s A : Set α} {t : Set β} {f : α → β},
  IsMulFreimanHom 2 s t f → Set.InjOn f s → A ⊆ s → ThreeGPFree (f '' A) → ThreeGPFree A
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A version of `Set.pi` for `AddSubmonoid`s. Given an index set `I` and a family
of `AddSubmonoid`s `s : Π i, AddSubmonoid f i`, `pi I s` is the `AddSubmonoid` of dependent
functions `f : Π i, f i` such that `f i` belongs to `pi I s` whenever `i ∈ I`.  -/
AddSubmonoid.pi : {ι : Type u_4} →
  {M : ι → Type u_5} →
    [inst : (i : ι) → AddZeroClass (M i)] → Set ι → ((i : ι) → AddSubmonoid (M i)) → AddSubmonoid ((i : ι) → M i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.aig : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput old → Std.Sat.AIG α
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableSub : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Sub α] [DiscreteMeasurableSpace α], MeasurableSub α
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mem_map_iff_mem : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ {S : Submonoid M} {x : M}, f x ∈ Submonoid.map f S ↔ x ∈ S
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isHexDigit_isEncodedChar : ∀ {r : UInt8 → Bool} {c : UInt8}, Std.Http.Internal.Char.isHexDigitByte c = true → Std.Http.URI.isEncodedChar r c = true
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Reindex a categorical coproduct via an equivalence of the index types.  -/
CategoryTheory.Limits.Sigma.reindex : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {γ : Type w'} →
        (ε : β ≃ γ) →
          (f : γ → C) →
            [inst_1 : CategoryTheory.Limits.HasCoproduct f] →
              [inst_2 : CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)] → ∐ f ∘ ⇑ε ≅ ∐ f
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.map_obj_as : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y))
  (x : FundamentalGroupoid X), ((FundamentalGroupoid.map f).obj x).as = f x.as
-- Init.Data.Option.Lemmas
Option.merge_eq_some_iff : ∀ {α : Type u_1} {o o' : Option α} {f : α → α → α} {a : α},
  Option.merge f o o' = some a ↔
    o = some a ∧ o' = none ∨ o = none ∧ o' = some a ∨ ∃ b c, o = some b ∧ o' = some c ∧ f b c = a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.mulLECancellable_val : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ), MulLECancellable ↑u
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.map_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A X Y : C} (i : A ⟶ X) [inst_1 : CategoryTheory.Mono i]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f],
  (CategoryTheory.Subobject.map f).obj (CategoryTheory.Subobject.mk i) =
    CategoryTheory.Subobject.mk (CategoryTheory.CategoryStruct.comp i f)
-- Std.Time.Duration
/-- Subtracts an `Hour.Offset` from a `Duration`
 -/
Std.Time.Duration.subHours : Std.Time.Duration → Std.Time.Hour.Offset → Std.Time.Duration
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_alter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {k k' : α},
  (↑m).WF →
    ∀ [inst_3 : Inhabited (β k')] {f : Option (β k) → Option (β k)},
      (m.alter k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).get! else m.get! k'