mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodSpec_coprodMk : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S]
  (x : ↥(AlgebraicGeometry.Spec (CommRingCat.of R)) ⊕ ↥(AlgebraicGeometry.Spec (CommRingCat.of S))),
  (AlgebraicGeometry.coprodSpec R S)
      ((AlgebraicGeometry.coprodMk (AlgebraicGeometry.Spec (CommRingCat.of R))
          (AlgebraicGeometry.Spec (CommRingCat.of S)))
        x) =
    (PrimeSpectrum.primeSpectrumProd R S).symm x
-- Mathlib.Topology.Algebra.Group.Basic
/-- The topological group isomorphism between the units of a product of two monoids, and the product
of the units of each monoid.  -/
Homeomorph.prodUnits : {α : Type u} →
  {β : Type v} →
    [inst : Monoid α] →
      [inst_1 : TopologicalSpace α] → [inst_2 : Monoid β] → [inst_3 : TopologicalSpace β] → (α × β)ˣ ≃ₜ αˣ × βˣ
-- Std.Data.Iterators.Lemmas.Combinators.Drop
Std.Iter.atIdxSlow?_drop : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Productive α Id] {k l : ℕ} {it : Std.Iter β},
  Std.Iter.atIdxSlow? l (Std.Iter.drop k it) = Std.Iter.atIdxSlow? (l + k) it
-- Lean.Parser.Term
Lean.Parser.Term.letDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.instIsIsoNeg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.AddGrpObj A], CategoryTheory.IsIso CategoryTheory.AddGrpObj.neg
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.Monic.geom_sum : ∀ {R : Type u} [inst : Semiring R] {P : Polynomial R},
  P.Monic → 0 < P.natDegree → ∀ {n : ℕ}, n ≠ 0 → (∑ i ∈ Finset.range n, P ^ i).Monic
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (ea eb : Lean.Grind.AC.Expr),
  sizeOf (Lean.Meta.Grind.AC.DiseqCnstrProof.core a b ea eb) = 1 + sizeOf a + sizeOf b + sizeOf ea + sizeOf eb
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_pos_iff_support_of_nonneg_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ᵐ[μ] f → MeasureTheory.Integrable f μ → (0 < ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f))
-- Init.Data.List.Nat.Modify
List.modifyTailIdx_add : ∀ {α : Type u_1} (f : List α → List α) (i : ℕ) (l₁ l₂ : List α),
  (l₁ ++ l₂).modifyTailIdx (l₁.length + i) f = l₁ ++ l₂.modifyTailIdx i f
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.WeakRankFunction.mk.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] (rank rank_1 : ↑P.II → α)
  (e_rank : rank = rank_1) (lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank x < rank y),
  { rank := rank, lt := lt } = { rank := rank_1, lt := ⋯ }
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_card : ∀ (a : Ordinal.{v}), Cardinal.lift.{u, v} a.card = (Ordinal.lift.{u, v} a).card
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.exists_minimal : ∀ {α : Type u_6} [inst : Preorder α] {s : Set α},
  (s.WellFoundedOn fun x1 x2 => x1 < x2) → s.Nonempty → ∃ a, Minimal (fun x => x ∈ s) a
-- Mathlib.SetTheory.ZFC.Class
Class.mem_asymm : ∀ {x y : Class.{u_1}}, x ∈ y → y ∉ x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Pos.skip?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String} {pos : s.Pos},
  pos.toSlice.skip? pat = Option.map String.Pos.toSlice (pos.skip? pat)
-- Mathlib.Algebra.DirectSum.Module
/-- `iff` version of `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top`,
`DirectSum.IsInternal.iSupIndep`, and `DirectSum.IsInternal.submodule_iSup_eq_top`.  -/
DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] (A : ι → Submodule R M), DirectSum.IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {X_1 Y Z : F.DescentData' sq sq₃} (f_1 : X_1 ⟶ Y) (g : Y ⟶ Z) (i : ι),
  (CategoryTheory.CategoryStruct.comp f_1 g).hom i = CategoryTheory.CategoryStruct.comp (f_1.hom i) (g.hom i)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.map_num : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] {𝒜 : ι → σ} {B : Type u_4} {τ : Type u_5} [inst_3 : CommRing B] [inst_4 : SetLike τ B]
  [inst_5 : AddSubgroupClass τ B] {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) {W₁ : Submonoid A} {W₂ : Submonoid B}
  (hw : W₁ ≤ Submonoid.comap f W₂) (c : HomogeneousLocalization.NumDenSameDeg 𝒜 W₁),
  (HomogeneousLocalization.NumDenSameDeg.map f hw c).num = (f.gradedAddHom c.deg) c.num
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
/-- The inclusion map `ℍ → ℂ` is a map of `C^n` manifolds.  -/
UpperHalfPlane.contMDiff_coe : ∀ {n : WithTop ℕ∞}, ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n UpperHalfPlane.coe
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.mk_eq_zero : ∀ {z : ℂ} (hz : ‖z‖ ≤ 1), Complex.UnitClosedDisc.mk z hz = 0 ↔ z = 0
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.vadd : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : VAdd M X] [ContinuousVAdd M X] {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X},
  Filter.Tendsto f l (nhds c) → Filter.Tendsto g l (nhds a) → Filter.Tendsto (fun x => f x +ᵥ g x) l (nhds (c +ᵥ a))
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.Sign.instReflBEq_batteries : ReflBEq Float.Model.UnpackedFloat.Sign
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightId_hom_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.mapRightId R L).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (s : Finset α) (n : ℕ), ↑(n • s) = n • ↑s
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting_eq_zero_iff : ∀ {n : ℕ}, n.primeCounting = 0 ↔ n ≤ 1
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.reduceProjFn? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_le_size_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, (↑m).size ≤ (↑(m.erase k)).size + 1
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.mk.sizeOf_spec : ∀ {ρ : Type} {pat : ρ} {s : String.Slice} [inst : SizeOf ρ] (currPos : s.Pos),
  sizeOf { currPos := currPos } = 1 + sizeOf currPos
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldlM.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} {δ : Type u_4} (motive : δ → Std.DHashMap.Internal.AssocList α β → Sort u_3) (d : δ)
  (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β)
  (h_1 : (d : δ) → motive d Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (d : δ) →
      (a : α) →
        (b : β a) →
          (es : Std.DHashMap.Internal.AssocList α β) → motive d (Std.DHashMap.Internal.AssocList.cons a b es)),
  (match d, Std.DHashMap.Internal.AssocList.cons a b es with
    | d, Std.DHashMap.Internal.AssocList.nil => h_1 d
    | d, Std.DHashMap.Internal.AssocList.cons a b es => h_2 d a b es) =
    h_2 d a b es
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.dfinsuppProd : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Add M] [inst_2 : CommMonoid M]
  [inst_3 : (i : ι) → Zero (β i)] [inst_4 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : RingCon M)
  (h h' : (i : ι) → β i → M) {f g : Π₀ (i : ι), β i},
  (∀ (i : ι), c (h i 0) 1) →
    (∀ (i : ι), c (h' i 0) 1) → (∀ (i : ι), c (h i (f i)) (h' i (g i))) → c (f.prod h) (g.prod h')
-- Lean.Meta.HasNotBit
/-- Is `e` a `hasNotBit` type that can be refuted?
Then return an expression that's the negation of it.
(This is used by `contradiction`)
 -/
Lean.refutableHasNotBit? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
summable_of_isBigO' : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [CompleteSpace E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ι → E} {g : ι → F},
  Summable g → f =O[Filter.cofinite] g → Summable f
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r_one_pow : ∀ {n : ℕ} (k : ℕ), DihedralGroup.r 1 ^ k = DihedralGroup.r ↑k
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  {D₁ D₂ : F.DescentData f}
  (φ φ_1 :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂),
  φ = φ_1 →
    ∀ ⦃i : ι⦄ {Z : C} (q : Z ⟶ X i) ⦃j : ι'⦄ (a a_1 : Z ⟶ X' j) (e_a : a = a_1)
      (fac : CategoryTheory.CategoryStruct.comp a (f' j) = CategoryTheory.CategoryStruct.comp q (f i)),
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ q a fac =
        CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ_1 q a_1 ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category
with `X` strictly `≤ b`, and `Y` strictly `≥ a` and `≤ b`
can be written as `f = Q.map g ≫ inv (Q.map s)` with `g : X ⟶ Y'` and
`s : Y ⟶ Y'` a quasi-isomorphism with `Y'` strictly `≥ a` and `≤ b`.  -/
DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : CochainComplex C ℤ} (a b : ℤ) [X.IsStrictlyLE b] [Y.IsStrictlyGE a]
  [Y.IsStrictlyLE b] (f : DerivedCategory.Q.obj X ⟶ DerivedCategory.Q.obj Y),
  ∃ Y',
    ∃ (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b),
      ∃ g s,
        ∃ (x : CategoryTheory.IsIso (DerivedCategory.Q.map s)),
          f =
            CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map g) (CategoryTheory.inv (DerivedCategory.Q.map s))
-- Batteries.Data.UInt
UInt16.ext : ∀ {x y : UInt16}, x.toNat = y.toNat → x = y
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats.tailSize : Lean.PersistentArray.Stats → ℕ
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.eq_bot_of_card_le : ∀ {M : Type u_1} [inst : AddMonoid M] {S : AddSubmonoid M} [inst_1 : Fintype ↥S], Fintype.card ↥S ≤ 1 → S = ⊥
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- Let `K` be a field with an admissible family of absolute values (giving rise
to a multiplicative height).
Let `p` be a family (indexed by `ι'`) of homogeneous polynomials in variables indexed by
the finite type `ι` and of the same degree `N`. Then for any `x : ι →  K`,
the multiplicative height of `fun j : ι' ↦ eval x (p j)` is bounded by a positive constant
(which is made explicit) times `mulHeight x ^ N`.  -/
Height.mulHeight_eval_le : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K] [Finite ι']
  [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K},
  (∀ (i : ι'), (p i).IsHomogeneous N) →
    ∀ (x : ι → K),
      (Height.mulHeight fun j => (MvPolynomial.eval x) (p j)) ≤ max (Height.mulHeightBound p) 1 * Height.mulHeight x ^ N
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_inv_hom_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) {Z : D}
  (h : Opposite.unop (F.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (CategoryTheory.CategoryStruct.comp (e.hom.app X).unop h) = h
-- Mathlib.Topology.Maps.Basic
IsOpenMap.preimage_frontier_eq_frontier_preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → Continuous f → ∀ (s : Set Y), f ⁻¹' frontier s = frontier (f ⁻¹' s)
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- Given lower bounds on non-adjacencies from `W` into `X`,`Xᶜ` we can bound the degree sum over `W`.
 -/
_private.Mathlib.Combinatorics.SimpleGraph.FiveWheelLike.0.SimpleGraph.sum_degree_le_of_le_not_adj : ∀ {α : Type u_1} {G : SimpleGraph α} {i j : ℕ} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj]
  {W X : Finset α},
  (∀ x ∈ X, i ≤ {z ∈ W | ¬G.Adj x z}.card) →
    (∀ y ∈ Xᶜ, j ≤ {z ∈ W | ¬G.Adj y z}.card) → ∑ w ∈ W, G.degree w ≤ X.card * (W.card - i) + Xᶜ.card * (W.card - j)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.instZero.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β],
  OrderAddMonoidHom.instZero =
    {
      zero :=
        let __src := 0;
        { toAddMonoidHom := __src, monotone' := ⋯ } }
-- Mathlib.CategoryTheory.Sites.LocallyBijective
/-- Given a category `C` equipped with a Grothendieck topology `J` and a concrete category `A`,
this property holds if a morphism in `Cᵒᵖ ⥤ A` satisfies `J.W` (i.e. becomes an iso after
sheafification) iff it is both locally injective and locally surjective.  -/
CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C →
      (A : Type u') →
        [inst : CategoryTheory.Category.{v', u'} A] →
          {FA : A → A → Type u_1} →
            {CA : A → Type w'} →
              [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] → [CategoryTheory.ConcreteCategory A FA] → Prop
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- `X.cycles` also identifies to a cokernel. More precisely,
`Z^n(f, g)` identifies to the cokernel of `H^n(f) ⟶ H^n(f ≫ g)`  -/
CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    (h : CategoryTheory.CategoryStruct.comp f g = fg) →
                      (n : ℤ) →
                        CategoryTheory.Limits.cokernel
                            ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) ≅
                          X.cycles f g n
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.mono_of_mono_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L),
  (∀ (i : ι), CategoryTheory.Mono (φ.f i)) → CategoryTheory.Mono φ
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.AssocListIterator.l : {α : Type u} →
  {β : α → Type v} → Std.DHashMap.Internal.AssocList.AssocListIterator α β → Std.DHashMap.Internal.AssocList α β
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LHom.onBoundedFormula.eq_5 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (g : L →ᴸ L') (x : ℕ)
  (f : L.BoundedFormula α (x + 1)), g.onBoundedFormula f.all = (g.onBoundedFormula f).all
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sigma.dist_triangle : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] (x y z : (i : ι) × E i),
  dist x z ≤ dist x y + dist y z
-- Init.Data.Float.Float32
/-- Bit-for-bit conversion to `UInt32`. Interprets a `Float32` as a `UInt32`, ignoring the numeric value
and treating the `Float32`'s bit pattern as a `UInt32`.

`Float32`s and `UInt32`s have the same endianness on all supported platforms. IEEE 754 very
precisely specifies the bit layout of floats.

This function is distinct from `Float.toUInt32`, which attempts to preserve the numeric value rather
than reinterpreting the bit pattern.
 -/
Float32.toBits : Float32 → UInt32
-- Init.SizeOf
Fin.mk.congr_simp : ∀ {n : ℕ} (val val_1 : ℕ) (e_val : val = val_1) (isLt : val < n), ⟨val, isLt⟩ = ⟨val_1, ⋯⟩
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.const_sub : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableSub G], AEMeasurable f μ → ∀ (c : G), AEMeasurable (fun x => c - f x) μ
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabInitQuot : Lean.Elab.Command.CommandElab
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (n : ℤ) (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (match Lean.Grind.CommRing.Expr.num n with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | x => h_3 x) =
    h_1 n
-- Init.Data.List.MinMaxOn
List.le_apply_maxOn_append_left : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (h : xs ≠ []), f (List.maxOn f xs h) ≤ f (List.maxOn f (xs ++ ys) ⋯)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.data? : Lean.Lsp.ResolvableCompletionItem → Option Lean.Lsp.ResolvableCompletionItemData
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.termπ_ : Lean.ParserDescr
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instIsRightCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsRightCancelAdd α], IsRightCancelAdd (Lex α)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_add_measure_compl : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → μ s + μ sᶜ = μ Set.univ
-- Mathlib.Topology.Sets.VietorisTopology
Topology.IsOpenEmbedding.nonemptyCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Topology.IsOpenEmbedding f), Topology.IsOpenEmbedding (TopologicalSpace.NonemptyCompacts.map f ⋯)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_idemFst_sup_idemSnd : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x : WithLp ⊤ (α × β)), ‖x‖ = max ‖WithLp.idemFst x‖ ‖WithLp.idemSnd x‖
-- Mathlib.Data.Nat.Nth
/-- `Nat.nth p` is the unique strictly monotone function whose image is `Set.ofPred p`.  -/
Nat.eq_nth_of_strictMonoOn_of_mapsTo_of_surjOn : ∀ {p : ℕ → Prop} (f : ℕ → ℕ),
  Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} (Set.ofPred p) →
    Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} (Set.ofPred p) →
      StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} →
        Set.EqOn f (Nat.nth p) {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card}
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instVAddAssocClass'' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M N] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddAssocClass M N α], VAddAssocClass M N (Lex α)
-- Mathlib.CategoryTheory.Iso
/-- Composition of the two directions of an isomorphism in reverse order
is the identity on the target.  -/
CategoryTheory.Iso.inv_hom_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.inv (CategoryTheory.CategoryStruct.comp self.hom h) = h
-- Mathlib.Topology.Algebra.InfiniteSum.Group
multipliable_iff_tprod_vanishing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] {f : β → α}
  [CompleteSpace α], Multipliable f ↔ ∀ e ∈ nhds 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_self_closure`.

---

The Hausdorff edistance between a set and its closure vanishes.  -/
EMetric.hausdorffEdist_self_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Metric.hausdorffEDist s (closure s) = 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X'),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.rightUnitor X').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instIsRegularEpiπ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (g h : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair g h)],
  CategoryTheory.IsRegularEpi (CategoryTheory.Limits.coequalizer.π g h)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.piUnique_apply : ∀ {ι : Type u_16} (M : ι → Type u_17) [inst : (j : ι) → Add (M j)] [inst_1 : Unique ι] (f : (i : ι) → M i),
  (AddEquiv.piUnique M) f = f default
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.instInhabited : {L : FirstOrder.Language} → Inhabited (L →ᴸ L)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.exClosure.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (φ : L.Formula α),
  φ.exClosure =
    FirstOrder.Language.Formula.iExs (↥(FirstOrder.Language.BoundedFormula.freeVarFinset φ))
      (FirstOrder.Language.Formula.relabel Sum.inr (FirstOrder.Language.BoundedFormula.restrictFreeVar φ id))
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  {x y : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ}, x.app = y.app → x = y
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAtFilter.sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → HasDerivAtFilter g g' L → HasDerivAtFilter (f - g) (f' - g') L
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_add_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionRing α] {q r : ℚ}, ↑q.den ≠ 0 → ↑r.den ≠ 0 → ↑(q + r) = ↑q + ↑r