mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.GaloisConnection.Defs
/-- A Galois insertion is a Galois connection where `l ∘ u = id`. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual
to `GaloisCoinsertion`  -/
GaloisInsertion : {α : Type u_2} → {β : Type u_3} → [Preorder α] → [Preorder β] → (α → β) → (β → α) → Type (max u_2 u_3)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Answer.size : Lean.Meta.SynthInstance.Answer → ℕ
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.nndist_eq_iSup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)}, nndist f g = ⨆ x, nndist (f x) (g x)
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.uncurry_apply : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B] (c : A →ₗ[R] CharacterModule B),
  CharacterModule.uncurry c = TensorProduct.liftAddHom c.toAddMonoidHom ⋯
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_smul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {R : Type u_10} [inst : SMul R α] (r : R)
  (A : Matrix m n α), (r • A).submatrix = r • A.submatrix
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.discreteTopology_pi_basisFun : ∀ {ι : Type u_2} [inst : Finite ι], DiscreteTopology ↥(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_neg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (s : NonemptyInterval α), (-s).toProd.1 = -s.toProd.2
-- Mathlib.Analysis.Fourier.AddCircle
/-- The `n`-th Fourier coefficient of a function `AddCircle T → E`, for `E` a complete normed
`ℂ`-vector space, defined as the integral over `AddCircle T` of `fourier (-n) t • f t`.  -/
fourierCoeff : {T : ℝ} →
  [hT : Fact (0 < T)] → {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (AddCircle T → E) → ℤ → E
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.limitIsoOfIsRightKanExtension_hom_π : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] [inst_4 : CategoryTheory.Limits.HasLimit F]
  [inst_5 : CategoryTheory.Limits.HasLimit F'] (i : C),
  CategoryTheory.CategoryStruct.comp (F'.limitIsoOfIsRightKanExtension α).hom (CategoryTheory.Limits.limit.π F i) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F' (L.obj i)) (α.app i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_le_maxKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {he : t.isEmpty = false}, (cmp (t.maxKey he) ((t.insert k v).maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.instOfPreservesColimitsOfShapeDiscreteWalkingPairOfReflectsMonomorphismsForget : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type u_3)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
      (CategoryTheory.forget C)]
  [(CategoryTheory.forget C).ReflectsMonomorphisms], CategoryTheory.Limits.MonoCoprod C
-- Init.Data.SInt.Lemmas
Int32.toInt_lt : ∀ (x : Int32), x.toInt < 2 ^ 31
-- Lean.Elab.Tactic.Simp
/-- Elaborates a `dsimp` configuration, which uses only a subset of the options
of a `simp` configuration. The `elabSimpConfig` function calls this and immediately
converts the result to a `Simp.Config`.  -/
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.elabDSimpConfigCore : Lean.Syntax →
  optParam Lean.Meta.DSimp.ConfigWithOptions { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Meta.DSimp.ConfigWithOptions
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.MonoidalCategory.tensoringRight_η : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.MonoidalCategory.tensoringRight C) =
    (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).hom
-- Init.Data.Vector.Lemmas
Vector.exists_mem_push : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {a : α} {xs : Vector α n},
  (∃ x, ∃ (_ : x ∈ xs.push a), p x) ↔ p a ∨ ∃ x, ∃ (_ : x ∈ xs), p x
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instRightDistribClass : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [RightDistribClass R], RightDistribClass (Lex R)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The second projection within a domain at a point in a product is `C^∞`.  -/
contDiffWithinAt_snd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {s : Set (E × F)} {p : E × F}, ContDiffWithinAt 𝕜 n Prod.snd s p
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_le : ∀ {x : ℤ} {m : ℕ}, 0 < m → x.bmod m ≤ (↑m - 1) / 2
-- Mathlib.Data.List.Sigma
List.kinsert_nodupKeys : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)},
  l.NodupKeys → (List.kinsert a b l).NodupKeys
-- Lean.CoreM
/-- Execute `x`, and apply `f` to the produced error message  -/
Lean.Core.mapError : {m : Type → Type u_1} →
  {α : Type} → [MonadControlT Lean.CoreM m] → [Monad m] → m α → (Lean.MessageData → Lean.MessageData) → m α
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkSizeOfSpecTheorem : Lean.InductiveVal → Array Lean.Name → Lean.NameMap Lean.Name → Lean.Name → Lean.MetaM Unit
-- Mathlib.Topology.Algebra.Support
mulTSupport_binop_subset : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : One α] [inst_1 : TopologicalSpace X]
  [inst_2 : One β] [inst_3 : One γ] (op : α → β → γ),
  op 1 1 = 1 → ∀ (f : X → α) (g : X → β), (mulTSupport fun x => op (f x) (g x)) ⊆ mulTSupport f ∪ mulTSupport g
-- Init.Data.BitVec.Lemmas
/-- Divide-and-conquer implementation of `BitVec.flattenList`, swapped in at runtime
via `@[csimp]`. See `BitVec.flattenList.toNatAux` for the cost analysis.
 -/
BitVec.flattenListFast : {n : ℕ} → (xs : List (BitVec n)) → BitVec (n * xs.length)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (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) (n : ℤ),
  a = Lean.Grind.CommRing.Expr.num n →
    (match a 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
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The pointwise multiplication of sets `s * t` and `t` is defined as `{x * y | x ∈ s, y ∈ t}` in
scope `Pointwise`.  -/
Set.mul : {α : Type u_2} → [Mul α] → Mul (Set α)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `OmegaCompletePartialOrder.Chain.zip` pairs up the elements of two chains
that have the same index.  -/
OmegaCompletePartialOrder.Chain.zip : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        OmegaCompletePartialOrder.Chain α → OmegaCompletePartialOrder.Chain β → OmegaCompletePartialOrder.Chain (α × β)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isFunLike : Lean.Expr → Lean.MetaM Bool
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_erase_le_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k km kme : α}
  (hkme : (t.erase k).max? = some kme), t.max?.get ⋯ = km → (cmp kme km).isLE = true
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`.  -/
CategoryTheory.Center.whiskerRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X₁ X₂ : CategoryTheory.Center C} → (X₁ ⟶ X₂) → (Y : CategoryTheory.Center C) → X₁.tensorObj Y ⟶ X₂.tensorObj Y
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.finrank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℝ (NumberField.mixedEmbedding.euclidean.mixedSpace K) = Module.finrank ℚ K
-- Mathlib.CategoryTheory.GlueData
/-- Objects of a glue data to be glued.  -/
CategoryTheory.GlueData'.U : {C : Type u₁} → [inst : CategoryTheory.Category.{v, u₁} C] → (self : CategoryTheory.GlueData' C) → self.J → C
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C]
  (property : ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X))
  (iff_shrink : ∀ {X : C} {E : CategoryTheory.PreZeroHypercover X}, property E ↔ property E.shrink),
  sizeOf { property := property, iff_shrink := iff_shrink } = 1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec.sizeOf_spec : ∀ (h : Lean.FVarId), sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec h) = 1 + sizeOf h
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_prod_of_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R}
  {s : Finset ι},
  (∀ i ∈ s, m.leadingCoeff (P i) ∈ nonZeroDivisors R) → m.leadingCoeff (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
-- Init.Tactics
/-- Syntax for using all lemmas labelled with an attribute in `solve_by_elim`.  -/
Lean.Parser.Tactic.SolveByElim.using_ : Lean.ParserDescr
-- Batteries.Data.AssocList
Batteries.AssocList.foldlM.eq_1 : ∀ {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : δ → α → β → m δ) (x : δ),
  Batteries.AssocList.foldlM f x Batteries.AssocList.nil = pure x
-- Init.Data.BitVec.Bootstrap
BitVec.neg.eq_1 : ∀ {n : ℕ} (x : BitVec n), x.neg = BitVec.ofNat n (2 ^ n - x.toNat)
-- Init.Data.Int.Lemmas
Int.neg_eq_zero : ∀ {a : ℤ}, -a = 0 ↔ a = 0
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Shrink the Picard-Lindelöf parameters to a smaller ball and time interval. The new radius `a'`
and initial deviation `r'` can be chosen freely as long as `a' ≤ a` and the time constraint
`L * max (tmax' - t₀') (t₀' - tmin') ≤ a' - r'` is satisfied.  -/
IsPicardLindelof.shrink : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax tmin' tmax' : ℝ} {t₀ : ↑(Set.Icc tmin tmax)}
  {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∀ (t₀' : ↑(Set.Icc tmin' tmax')),
      tmin ≤ tmin' →
        tmax' ≤ tmax →
          ∀ {a' r' : NNReal},
            a' ≤ a → ↑L * max (tmax' - ↑t₀') (↑t₀' - tmin') ≤ ↑a' - ↑r' → IsPicardLindelof f t₀' x₀ a' r' L K
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
/-- Every transvection in `SL ι F` whose indices are `(i₁, i₂)` or `(i₂, i₁)` is in the join
of `lineStab(span F {e_{i₁}})` and `lineStab(span F {e_{i₂}})`.  -/
SL2Gen.transvection_mem_lineStab_sup : ∀ {F : Type u_2} [inst : Field F] (t : Matrix.TransvectionStruct (Fin 2) F),
  t.toSpecialLinearGroup ∈
    Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single 0 1) ⊔ Matrix.SpecialLinearGroup.lineStab (F ∙ Pi.single 1 1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).getKey? a = none
-- Mathlib.NumberTheory.Dioph
Poly.sumsq_eq_zero : ∀ {α : Type u_1} (x : α → ℕ) (l : List (Poly α)), (Poly.sumsq l) x = 0 ↔ List.Forall (fun a => a x = 0) l
-- Mathlib.Topology.Algebra.Group.Basic
topologicalGroup_iInf : ∀ {G : Type w} {ι : Sort u_1} [inst : Group G] {ts' : ι → TopologicalSpace G},
  (∀ (i : ι), IsTopologicalGroup G) → IsTopologicalGroup G
-- Mathlib.Data.EReal.Basic
EReal.coe_mul : ∀ (x y : ℝ), ↑(x * y) = ↑x * ↑y
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.tensorEquivSum_one_tmul_X : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {ι : Type u_2} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (i : ι),
  (MvPolynomial.tensorEquivSum R σ ι S) (1 ⊗ₜ[R] MvPolynomial.X i) = MvPolynomial.X (Sum.inr i)
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshRef.mk.sizeOf_spec : ∀ (ref : IO.Ref ProofWidgets.RefreshComponent.RefreshState), sizeOf { ref := ref } = 1 + sizeOf ref
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.restrict_toMeasure_support : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α), p.toMeasure.restrict p.support = p.toMeasure
-- Mathlib.LinearAlgebra.Orientation
/-- The orientation given by a basis.  -/
Module.Basis.orientation : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommGroup M] →
            [inst_4 : Module R M] →
              {ι : Type u_4} → [Fintype ι] → [DecidableEq ι] → Module.Basis ι R M → Orientation R M ι
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.coe_div : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] (x y : ↥H),
  ↑(x / y) = ↑x / ↑y
-- Init.Grind.Module.OfNatModule
Lean.Grind.IntModule.OfNatModule.of_le : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α] {a b : α} {a' b' : Lean.Grind.IntModule.OfNatModule.Q α},
  Lean.Grind.IntModule.OfNatModule.toQ a = a' → Lean.Grind.IntModule.OfNatModule.toQ b = b' → a ≤ b → a' ≤ b'
-- Mathlib.Data.Finset.Prod
/-- Given a finite set `s`, the diagonal, `s.diag` is the set of pairs of the form `(a, a)` for
`a ∈ s`.  -/
Finset.diag : {α : Type u_1} → Finset α → Finset (α × α)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.smul_Icc : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] [MulLeftReflectLE α]
  [ExistsMulOfLE α] (a b c : α), a • Set.Icc b c = Set.Icc (a * b) (a * c)
-- Mathlib.Data.Num.Basic
PosNum.brecOn.go : {motive : PosNum → Sort u} → (t : PosNum) → ((t : PosNum) → PosNum.below t → motive t) → motive t ×' PosNum.below t
-- Init.Core
/-- Depends on the correctness of the Lean compiler, interpreter, and all `[implemented_by ...]` and `[extern ...]` annotations.
 -/
Lean.trustCompiler : True
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
/-- The map `KaehlerDifferential f ⟶ (ModuleCat.restrictScalars g').obj (KaehlerDifferential f')`
induced by a commutative square (given by an equality `g ≫ f' = f ≫ g'`)
in the category `CommRingCat`.  -/
CommRingCat.KaehlerDifferential.map : {A B A' B' : CommRingCat} →
  {f : A ⟶ B} →
    {f' : A' ⟶ B'} →
      {g : A ⟶ A'} →
        {g' : B ⟶ B'} →
          CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g' →
            (CommRingCat.KaehlerDifferential f ⟶
              (ModuleCat.restrictScalars (CommRingCat.Hom.hom g')).obj (CommRingCat.KaehlerDifferential f'))
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.iterate_omega0_opow_lt_epsilon_zero`.

---

`ω ^ ω ^ … ^ 0 < ε₀`  -/
Ordinal.iterate_omega0_opow_lt_epsilon0 : ∀ (n : ℕ), (fun a => Ordinal.omega0 ^ a)^[n] 0 < Ordinal.epsilon 0
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.neg_le_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommGroup M] [Lean.Grind.OrderedAdd M]
  {a b : M}, -a ≤ b ↔ -b ≤ a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β},
  k ∉ t₂ → Std.ExtDTreeMap.Const.getD (t₁ \ t₂) k fallback = Std.ExtDTreeMap.Const.getD t₁ k fallback
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_map_of_map_zero : ∀ (f : CircleDeg1Lift) (x : ℝ), f 0 + ↑⌊x⌋ ≤ f x
-- Init.Data.Array.Range
Array.range'_eq_map_range : ∀ {s n : ℕ}, Array.range' s n = Array.map (fun x => s + x) (Array.range n)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.one_lt_two : 1 < 2
-- Mathlib.Logic.Equiv.Sum
/-- If `α ≃ α'` and `β ≃ β'`, then `α ⊕ β ≃ α' ⊕ β'`. This is `Sum.map` as an equivalence.  -/
Equiv.sumCongr : {α₁ : Type u_9} → {α₂ : Type u_10} → {β₁ : Type u_11} → {β₂ : Type u_12} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_closure : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (s : Set Rᵐᵒᵖ),
  (Subsemiring.closure s).unop = Subsemiring.closure (MulOpposite.op ⁻¹' s)
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.Props.mk.sizeOf_spec : ∀ (contents : String), sizeOf { contents := contents } = 1 + sizeOf contents
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.mk : ℕ →
  Lean.Expr →
    Lean.Level →
      Lean.Expr →
        Option Lean.Expr →
          Lean.Expr →
            Option Lean.Expr →
              Option Lean.Expr →
                Option Lean.Expr →
                  ℕ →
                    Lean.PArray Lean.Expr →
                      Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Var →
                        Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Expr →
                          Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr) →
                            Lean.Meta.Grind.AC.Queue →
                              List Lean.Meta.Grind.AC.EqCnstr →
                                Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr → Bool → Lean.Meta.Grind.AC.Struct
-- Mathlib.Order.Minimal
Maximal.mem_of_prop_insert : ∀ {α : Type u_2} {x : α} {P : Set α → Prop} {s : Set α}, Maximal P s → P (insert x s) → x ∈ s
-- Lean.Elab.Do.Control
Lean.Elab.Do.EffectForwarder.mk : Lean.Elab.Do.DoElemCont →
  Option Lean.Elab.Do.ControlStack →
    Option Lean.Elab.Do.ControlStack →
      Option Lean.Elab.Do.ControlStack → Lean.Elab.Do.ControlStack → Lean.Expr → Lean.Elab.Do.EffectForwarder
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.ExprConfigCacheKey.mk : Lean.Expr → UInt64 → Lean.Meta.ExprConfigCacheKey
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.le_add_right : ∀ {σ : Type u_1} (m : MonomialOrder σ) (a b : σ →₀ ℕ), m.toSyn a ≤ m.toSyn a + m.toSyn b
-- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
/-- **Integration by parts for Fréchet derivatives**
Version with a general bilinear form `B`.
If `B f g` is integrable, as well as `B f' g` and `B f g'` where `f'` and `g'` are the derivatives
of `f` and `g` in a given direction `v`, then `∫ B f g' = - ∫ B f' g`.  -/
integral_bilinear_fderiv_right_eq_neg_left_of_integrable : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace ℝ W] [inst_8 : MeasurableSpace E] {μ : MeasureTheory.Measure E}
  [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {f : E → F} {g : E → G} {v : E} {B : F →L[ℝ] G →L[ℝ] W},
  MeasureTheory.Integrable (fun x => (B ((fderiv ℝ f x) v)) (g x)) μ →
    MeasureTheory.Integrable (fun x => (B (f x)) ((fderiv ℝ g x) v)) μ →
      MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ →
        (∀ x ∈ tsupport g, DifferentiableAt ℝ f x) →
          (∀ x ∈ tsupport f, DifferentiableAt ℝ g x) →
            ∫ (x : E), (B (f x)) ((fderiv ℝ g x) v) ∂μ = -∫ (x : E), (B ((fderiv ℝ f x) v)) (g x) ∂μ
-- Lean.Server.GoTo
Lean.Server.GoToM : Type → Type
-- Lean.Meta.Tactic.Grind.Types
/-- `withoutReportingMVarIssues x` executes `x` without reporting metavariables found during internalization.
See comment at `Grind.Context.reportMVarIssue` for additional details.
 -/
Lean.Meta.Grind.withoutReportingMVarIssues : {m : Type → Type u_1} → {α : Type} → [MonadControlT Lean.Meta.Grind.GrindM m] → [Monad m] → m α → m α
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Suprema of `X`-generated topologies are `X`-generated.  -/
Topology.IsGeneratedBy.sup : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {t₁ t₂ : TopologicalSpace Y},
  Topology.IsGeneratedBy X Y → Topology.IsGeneratedBy X Y → Topology.IsGeneratedBy X Y
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.map_inv_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Inv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant],
  MeasureTheory.Measure.map Inv.inv μ = μ
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_nat_mod : ∀ (s : Multiset ℕ) (n : ℕ), s.sum % n = (Multiset.map (fun x => x % n) s).sum % n
-- Init.Data.Vector.Lemmas
Vector.back?_flatMap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m},
  (xs.flatMap f).back? = Vector.findSome? (fun a => (f a).back?) xs.reverse
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.ext : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {x y : P.Cotangent}, x.val = y.val → x = y
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldl_loop_lt : ∀ {α : Sort u_1} {n i : ℕ} (f : α → Fin n → α) (x : α) (h : i < n),
  Fin.foldl.loop n f x i = Fin.foldl.loop n f (f x ⟨i, h⟩) (i + 1)
-- Mathlib.RingTheory.AdicCompletion.Basic
Hausdorffification.lift_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N) (x : M),
  (Hausdorffification.lift I f) ((Hausdorffification.of I M) x) = f x
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_eq_mabs : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] {a b : α}, |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹
-- Mathlib.Algebra.Group.Defs
IsAddLeftRegular.add_eq_zero_symm : ∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, IsAddLeftRegular a → a + b = 0 → b + a = 0
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ext : ∀ {R : Type u_1} {inst : Semiring R} {x y : ValuativeRel R}, ValuativeRel.vle = ValuativeRel.vle → x = y
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.mfderivWithin_congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s t : Set M},
  MDiffAt[s] f x → (∀ x ∈ t, f₁ x = f x) → f₁ x = f x → UniqueMDiffAt[t] x → t ⊆ s → mfderiv[t] f₁ x = mfderiv[s] f x
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- `α` is equivalent to its image in `α ⊕ β` as measurable spaces.  -/
MeasurableEquiv.Set.rangeInl : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → ↑(Set.range Sum.inl) ≃ᵐ α