mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.pointwise_smul_subset_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Subsemiring R}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuousWithinAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s : Set α},
  LowerHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_zero_iff : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : ↑S.X₂),
  (CategoryTheory.ConcreteCategory.hom S.pOpcycles) x = 0 ↔ x ∈ (ModuleCat.Hom.hom S.f).range
-- Mathlib.Topology.Constructions
Pi.continuous_postcomp : ∀ {X : Type u} {Y : Type v} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {g : X → Y},
  Continuous g → Continuous fun x => g ∘ x
-- Mathlib.Probability.ProductMeasure
/-- Restricting the product measure to a product indexed by a finset yields the usual
product measure.  -/
MeasureTheory.Measure.infinitePiNat_map_restrict : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] (I : Finset ℕ),
  MeasureTheory.Measure.map I.restrict (MeasureTheory.Measure.infinitePiNat μ) = MeasureTheory.Measure.pi fun i => μ ↑i
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.sin_angle_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
    p₁ ≠ p₂ ∨ p₃ ≠ p₂ → Real.sin (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_vecAppend : ∀ {α : Type u} {m n o : ℕ} (ho : o + 1 = m + 1 + n) (x : α) (u : Fin m → α) (v : Fin n → α),
  Matrix.vecAppend ho (Matrix.vecCons x u) v = Matrix.vecCons x (Matrix.vecAppend ⋯ u v)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.id : Lean.Meta.Grind.AC.EqCnstr → ℕ
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_U_eval_one_recurrence : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ),
  (2 * ↑k + 3) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.U R n)) =
    ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n))
-- Mathlib.Analysis.SpecificLimits.Normed
summable_geometric_of_abs_lt_one : ∀ {r : ℝ}, |r| < 1 → Summable fun n => r ^ n
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.embDomainLinearMap_apply : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Semiring R] [inst_2 : PartialOrder Γ']
  (f : Γ ↪o Γ') (a : HahnSeries Γ R), (HahnSeries.embDomainLinearMap f) a = HahnSeries.embDomain f a
-- Init.Data.Vector.Lemmas
Vector.toArray_append : ∀ {α : Type u_1} {m n : ℕ} {xs : Vector α m} {ys : Vector α n}, (xs ++ ys).toArray = xs.toArray ++ ys.toArray
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- For an `R`-module `M`, the restriction of scalars of `M` by the identity morphism identifies
to `M`.  -/
ModuleCat.restrictScalarsId'App : {R : Type u₁} →
  [inst : Ring R] → (f : R →+* R) → f = RingHom.id R → (M : ModuleCat R) → (ModuleCat.restrictScalars f).obj M ≅ M
-- Mathlib.Data.Finset.Sups
Finset.infs_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁ ⊼ t ⊆ s₂ ⊼ t
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] {B : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} B] [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B)
  [inst_5 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_6 : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] (X : C)
  (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A) {Z : B} (h : F.obj (Φ.presheafFiber.obj P) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (P.comp F))
      (CategoryTheory.CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app P) h) =
    CategoryTheory.CategoryStruct.comp (F.map (Φ.toPresheafFiber X x P)) h
-- Mathlib.Order.Heyting.Hom
CoheytingHom.toFun_eq_coe_aux : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] {f : CoheytingHom α β},
  ⇑f.toLatticeHom = ⇑f
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.State : Type
-- Mathlib.RingTheory.Valuation.Integers
Valuation.leSubmodule_comap_algebraMap_eq_leIdeal : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [inst_1 : Field K] (v : Valuation K Γ₀)
  (γ : Γ₀), Submodule.comap (Algebra.linearMap (↥v.integer) K) (v.leSubmodule γ) = v.leIdeal γ
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_iff_le_liminf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  LowerSemicontinuous f ↔ ∀ (x : α), f x ≤ Filter.liminf f (nhds x)
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.card_uIcc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → Lattice (α i)] [inst_3 : (i : ι) → Zero (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)]
  (f g : Π₀ (i : ι), α i), (Finset.uIcc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.uIcc (f i) (g i)).card
-- Std.Internal.UV.TCP
/-- Connects a TCP socket to the specified address.
 -/
Std.Internal.UV.TCP.Socket.connect : Std.Internal.UV.TCP.Socket → Std.Net.SocketAddress → IO (IO.Promise (Except IO.Error Unit))
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.comp_app_assoc : ∀ {n : ℕ} {X Y Z : SSet.Truncated n} (f : X ⟶ Y) (g : Y ⟶ Z) (d : (SimplexCategory.Truncated n)ᵒᵖ) {Z_1 : Type u_1}
  (h : Z.obj d ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).app d) h =
    CategoryTheory.CategoryStruct.comp (f.app d) (CategoryTheory.CategoryStruct.comp (g.app d) h)
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- The characteristic map of an inclusion of presheaves.
Given a monomorphism of sheaves `m : F ⟶ G`, an object X of the site, map an element `x : G(X)`
to the (closed) sieve on X where `f : Y → X` is in the sieve iff
  `∃ a ∈ F(Y), G(f)(x) = m_Y(a)`
 -/
CategoryTheory.Presheaf.χ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} → (F ⟶ G) → (G ⟶ CategoryTheory.Functor.sieves C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ0_c₄ : ∀ (R : Type u_1) [inst : CommRing R], (WeierstrassCurve.ofJ0 R).c₄ = 0
-- Lean.Meta.Tactic.Grind.Types
/-- Pushes `a = True` with `proof` to `newEqs`.  -/
Lean.Meta.Grind.pushEqTrue : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.isCircuit_restrict_of_subset : ∀ {α : Type u_1} {M : Matroid α} {C R : Set α}, M.IsCircuit C → C ⊆ R → (M.restrict R).IsCircuit C
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toNonUnitalRingHom' : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R ≃+* S), ⇑f.toNonUnitalRingHom = ⇑f
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.Equiv.decidable.match_1.eq_1 : ∀ {α : Type u_1} (motive : Lists α → Lists α → Sort u_2) (l₁ l₂ : Lists' α false)
  (h_1 : (l₁ l₂ : Lists' α false) → motive ⟨false, l₁⟩ ⟨false, l₂⟩)
  (h_2 : (l₁ : Lists' α false) → (l₂ : Lists' α true) → motive ⟨false, l₁⟩ ⟨true, l₂⟩)
  (h_3 : (l₁ : Lists' α true) → (l₂ : Lists' α false) → motive ⟨true, l₁⟩ ⟨false, l₂⟩)
  (h_4 : (l₁ l₂ : Lists' α true) → motive ⟨true, l₁⟩ ⟨true, l₂⟩),
  (match ⟨false, l₁⟩, ⟨false, l₂⟩ with
    | ⟨false, l₁⟩, ⟨false, l₂⟩ => h_1 l₁ l₂
    | ⟨false, l₁⟩, ⟨true, l₂⟩ => h_2 l₁ l₂
    | ⟨true, l₁⟩, ⟨false, l₂⟩ => h_3 l₁ l₂
    | ⟨true, l₁⟩, ⟨true, l₂⟩ => h_4 l₁ l₂) =
    h_1 l₁ l₂
-- Mathlib.Algebra.Group.Defs
nsmulBinRecAuto.eq_1 : ∀ {M : Type u_2} [inst : AddSemigroup M] [inst_1 : Zero M] (k : ℕ) (m : M), nsmulBinRecAuto k m = nsmulBinRec k m
-- Init.Data.String.FindPos
String.Slice.posLE.eq_def : ∀ (s : String.Slice) (offset : String.Pos.Raw),
  s.posLE offset =
    if h' : String.Pos.Raw.IsValidForSlice s offset then s.pos offset h'
    else
      have this := ⋯;
      s.posLE offset.dec
-- Init.Data.BitVec.Lemmas
BitVec.false_cons_zero : ∀ {w : ℕ}, BitVec.cons false 0#w = 0#(w + 1)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mk_mem_nonZeroDivisors_associates : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] {a : M₀},
  Associates.mk a ∈ nonZeroDivisors (Associates M₀) ↔ a ∈ nonZeroDivisors M₀
-- Mathlib.Topology.Closure
Set.Finite.interior_sInter : ∀ {X : Type u} [inst : TopologicalSpace X] {S : Set (Set X)}, S.Finite → interior (⋂₀ S) = ⋂ s ∈ S, interior s
-- Init.Data.List.Perm
List.nil_perm : ∀ {α : Type u_1} {l₁ : List α}, [].Perm l₁ ↔ l₁ = []
-- Mathlib.Topology.Category.Profinite.Nobeling.Induction
/-- `GoodProducts C` as a `ℤ`-basis for `LocallyConstant C ℤ`.  -/
Profinite.NobelingProof.GoodProducts.Basis : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [WellFoundedLT I] → IsClosed C → Module.Basis ↑(Profinite.NobelingProof.GoodProducts C) ℤ (LocallyConstant ↑C ℤ)
-- Mathlib.Analysis.Complex.LocallyUniformLimit
TendstoLocallyUniformlyOn.deriv : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U : Set ℂ} {φ : Filter ι}
  {F : ι → ℂ → E} {f : ℂ → E} [CompleteSpace E],
  TendstoLocallyUniformlyOn F f φ U →
    (∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) → IsOpen U → TendstoLocallyUniformlyOn (deriv ∘ F) (deriv f) φ U
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_image_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  ⇑(P.reflection i) '' Set.range ⇑P.root = Set.range ⇑P.root
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_neg : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : SubtractionCommMonoid γ] {f : Π₀ (i : ι), β i}
  {h : (i : ι) → β i → γ}, (f.sum fun i b => -h i b) = -f.sum h
-- Init.Core
/-- Subset relation: `a ⊆ b`  

Conventions for notations in identifiers:

 * The recommended spelling of `⊆` in identifiers is `subset`. -/
«term_⊆_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.NoncommCoprod
AddMonoidHom.noncommCoprod_comp_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)),
  (f.noncommCoprod g comm).comp (AddMonoidHom.inr M N) = g
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.dist_lt_iff_of_compact : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β} {C : ℝ} [CompactSpace α],
  0 < C → (dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionObj_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] (d : Dᵒᵖ) (c : Cᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (Opposite.unop d) (Opposite.unop c) =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.pair_zero : ∀ {α : Type u_2} [inst : Preorder α] (a b : α) (hab : a ≤ b), (OmegaCompletePartialOrder.Chain.pair a b hab) 0 = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.epi_inr_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    autoParam (CategoryTheory.Epi f) CategoryTheory.IsPushout.epi_inr_of_epi._auto_1 → CategoryTheory.Epi inr
-- Mathlib.FieldTheory.CardinalEmb
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.instDecidableEqToTypeOrdRankSucc : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            (i : (Module.rank F E).ord.ToType) → Decidable (Order.succ i = i)
-- Std.Data.HashMap.Lemmas
Std.HashMap.fold_eq_foldl_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.HashMap.fold (fun d a x => f d a) init m = List.foldl f init m.keys
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.RewriteLemma.mk : Lean.Name → Bool → Mathlib.Tactic.LibraryRewrite.RewriteLemma
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
_private.Mathlib.Algebra.BigOperators.Group.List.Lemmas.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_iAlls : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : Finite β]
  {φ : L.Formula (α ⊕ β)} {v : α → M} {v' : Fin 0 → M},
  FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.Formula.iAlls β φ) v v' ↔
    ∀ (i : β → M), φ.Realize fun a => Sum.elim v i a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, k ∉ m₂ → (m₁ \ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.getKey? k =
    if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then some k else none
-- Init.Ext
Prod.ext : ∀ {α : Type u} {β : Type v} {x y : α × β}, x.1 = y.1 → x.2 = y.2 → x = y
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.epiModSerre_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  P.epiModSerre f
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommRing.mk.injEq : ∀ (toRing : Lean.Meta.Sym.Arith.Ring) (invFn? : Option Lean.Expr) (semiringId? : Option ℕ)
  (commSemiringInst commRingInst : Lean.Expr) (noZeroDivInst? fieldInst? : Option Lean.Expr)
  (toRing_1 : Lean.Meta.Sym.Arith.Ring) (invFn?_1 : Option Lean.Expr) (semiringId?_1 : Option ℕ)
  (commSemiringInst_1 commRingInst_1 : Lean.Expr) (noZeroDivInst?_1 fieldInst?_1 : Option Lean.Expr),
  ({ toRing := toRing, invFn? := invFn?, semiringId? := semiringId?, commSemiringInst := commSemiringInst,
        commRingInst := commRingInst, noZeroDivInst? := noZeroDivInst?, fieldInst? := fieldInst? } =
      { toRing := toRing_1, invFn? := invFn?_1, semiringId? := semiringId?_1, commSemiringInst := commSemiringInst_1,
        commRingInst := commRingInst_1, noZeroDivInst? := noZeroDivInst?_1, fieldInst? := fieldInst?_1 }) =
    (toRing = toRing_1 ∧
      invFn? = invFn?_1 ∧
        semiringId? = semiringId?_1 ∧
          commSemiringInst = commSemiringInst_1 ∧
            commRingInst = commRingInst_1 ∧ noZeroDivInst? = noZeroDivInst?_1 ∧ fieldInst? = fieldInst?_1)
-- Mathlib.Algebra.Order.UpperLower
upperClosure_mul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] (s t : Set α),
  ↑(upperClosure s) * t = ↑(upperClosure (s * t))
-- Mathlib.Analysis.Convex.Integral
/-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C`
a.e. on a set `t` of finite measure, then either this function is a.e. equal to its average value on
`t`, or the norm of its integral over `t` is strictly less than `μ.real t * C`.  -/
ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {t : Set α} {f : α → E} {C : ℝ} [StrictConvexSpace ℝ E],
  μ t ≠ ⊤ →
    (∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C) →
      f =ᵐ[μ.restrict t] Function.const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < μ.real t * C
-- Std.Async.Process
Std.IO.Process.instDecidableEqPId.decEq : (x x_1 : Std.IO.Process.PId) → Decidable (x = x_1)
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.steps? : Aesop.NormRuleResult → Option (Array Aesop.Script.LazyStep)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.ediam_image : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (s : Set α),
  Metric.ediam (⇑h '' s) = Metric.ediam s
-- Mathlib.LinearAlgebra.Determinant
/-- `Basis.det` is not the zero map.  -/
Module.Basis.det_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) [Nontrivial R], e.det ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.divOfHom_apply_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (g : Multiplicative G) (x : AddMonoidAlgebra k G), (AddMonoidAlgebra.divOfHom g) x = x.divOf (Multiplicative.toAdd g)
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_mod : ∀ (a b : BitVec 64), { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }
-- Mathlib.CategoryTheory.Idempotents.Biproducts
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_3 : Finite J]
  (F : J → CategoryTheory.Idempotents.Karoubi C),
  (CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).pt.X = ⨁ fun j => (F j).X
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.unit_pullbackComp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).unit
      ((CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g)).whiskerLeft
        (CategoryTheory.ChosenPullbacksAlong.pullbackComp f g).hom) =
    (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).unit
-- Mathlib.Tactic.Variable
/-- Get the type out of a bracketed binder.  -/
Mathlib.Command.Variable.bracketedBinderType : Lean.Syntax → Option Lean.Term
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- The bivariate polynomial `g(X) * f(Y) - f(X) * g(Y)`, where `f` and `g` are
the numerator and denominator of `generator`. This is an auxiliary definition
for the proof of Lüroth's theorem.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.θ : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → Polynomial (Polynomial K)
-- Mathlib.Order.SupClosed
latticeClosure_sup_inf_induction : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α} (p : (a : α) → a ∈ latticeClosure s → Prop),
  (∀ (a : α) (has : a ∈ s), p a ⋯) →
    (∀ (a : α) (has : a ∈ latticeClosure s) (b : α) (hbs : b ∈ latticeClosure s), p a has → p b hbs → p (a ⊔ b) ⋯) →
      (∀ (a : α) (has : a ∈ latticeClosure s) (b : α) (hbs : b ∈ latticeClosure s), p a has → p b hbs → p (a ⊓ b) ⋯) →
        ∀ {a : α} (has : a ∈ latticeClosure s), p a has
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw₀.beq.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  [inst_3 : (k : α) → BEq (β k)] (m₁ m₁_1 : Std.DHashMap.Internal.Raw₀ α β),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.DHashMap.Internal.Raw₀ α β), m₂ = m₂_1 → m₁.beq m₂ = m₁_1.beq m₂_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The pushout cocone obtained by flipping `inl` and `inr`.  -/
CategoryTheory.Limits.PushoutCocone.flip : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} → {g : X ⟶ Z} → CategoryTheory.Limits.PushoutCocone f g → CategoryTheory.Limits.PushoutCocone g f
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.one_smul_self_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] (X : C) [inst_3 : CategoryTheory.ModObj M X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Real.deriv_exp : deriv Real.exp = Real.exp
-- Mathlib.Data.Finset.Sups
Finset.sups_union_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s₁ s₂ t : Finset α},
  (s₁ ∪ s₂) ⊻ t = s₁ ⊻ t ∪ s₂ ⊻ t
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.trimLeft.go : {i : Type u_1} → List (Lean.Doc.Inline i) → String × Lean.Doc.Inline i
-- Mathlib.Data.Finset.Pi
Finset.restrict₂.congr_simp : ∀ {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} (hst : s ⊆ t) (f f_1 : (i : ↥t) → π ↑i),
  f = f_1 → ∀ (i : ↥s), Finset.restrict₂ hst f i = Finset.restrict₂ hst f_1 i
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffOn_finsum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {f : ι → M → G},
  (LocallyFinite fun i => Function.support (f i)) →
    (∀ (i : ι), ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (fun x => ∑ᶠ (i : ι), f i x) s