mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Given a pullback square assembled from a commuting square on the left and
a pullback square on the right, the left square is a pullback square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
|            |            |
v₁₁          v₁₂          v₁₃
↓            ↓            ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
 -/
CategoryTheory.IsPullback.of_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
  CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
      (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂) →
    CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁ →
      CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂ → CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_top : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M], ↑⊤ = Set.univ
-- Init.Data.String.Defs
String.instLTPos_1 : {s : String.Slice} → LT s.Pos
-- Mathlib.Order.Interval.Finset.Fin
Fin.instLocallyFiniteOrderBot : (n : ℕ) → LocallyFiniteOrderBot (Fin n)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instQuasiIsoAtIntιTruncLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ), QuasiIsoAt (K.ιTruncLE n) n
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_finsetSum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} {s : Finset ι}
  {v : ι → α →₀ M}, Finsupp.mapDomain f (∑ i ∈ s, v i) = ∑ i ∈ s, Finsupp.mapDomain f (v i)
-- Mathlib.Data.Part
Part.mk : {α : Type u} → (Dom : Prop) → (Dom → α) → Part α
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is a non-unital commutative
semiring.

See note [reducible non-instances].  -/
Algebra.adjoinCommSemiringOfComm : (R : Type uR) →
  {A : Type uA} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] → {s : Set A} → (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → CommSemiring ↥(Algebra.adjoin R s)
-- Mathlib.Data.Set.SMulAntidiagonal
Set.vaddAntidiagonal_mono_right : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s : Set G} {t₁ t₂ : Set P} {a : P},
  t₁ ⊆ t₂ → s.vaddAntidiagonal t₁ a ⊆ s.vaddAntidiagonal t₂ a
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mk : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {f : Polynomial R} →
            (map : Polynomial R →ₐ[R] S) →
              Function.Surjective ⇑map → RingHom.ker map = Ideal.span {f} → IsAdjoinRoot S f
-- Init.System.ST
ST.Prim.Ref.get : {σ α : Type} → ST.Ref σ α → ST σ α
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_hom_apply_app : ∀ (J : Type v) [inst : CategoryTheory.SmallCategory J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  (X : (CategoryTheory.Functor J C)ᵒᵖ) (X_1 : C)
  (a : CategoryTheory.Limits.limit ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X_1))) (j : J),
  ((CategoryTheory.ConcreteCategory.hom
            (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X).app X_1))
          a).app
      j =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X_1)) (Opposite.op j)))
      a
-- Mathlib.Data.List.Lemmas
List.mapAccumr.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ → γ × β) (x : List α) (x_1 : γ),
  List.mapAccumr f x x_1 =
    match x, x_1 with
    | [], c => (c, [])
    | y :: yr, c =>
      have r := List.mapAccumr f yr c;
      have z := f y r.1;
      (z.1, z.2 :: r.2)
-- Mathlib.MeasureTheory.Measure.Content
TopologicalSpace.Compacts.equiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  TopologicalSpace.Compacts.equiv f =
    { toFun := TopologicalSpace.Compacts.map ⇑f ⋯, invFun := TopologicalSpace.Compacts.map ⇑f.symm ⋯, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.subset_def : ∀ {x y : ZFSet.{u}}, x ⊆ y ↔ ∀ ⦃z : ZFSet.{u}⦄, z ∈ x → z ∈ y
-- Mathlib.Tactic.Sat.FromLRAT
/-- The core unit-propagation step.

We have a local context of assumptions `¬l'` (sometimes called an assignment)
and we wish to add `¬l` to the context, that is, we want to prove `l` is also falsified.
This is because there is a clause `a ∨ b ∨ ¬l` in the global context
such that all literals in the clause are falsified except for `¬l`;
so in the context `h₁` where we suppose that `¬l` is falsified,
the clause itself is falsified so we can prove `False`.
We continue the proof in `h₂`, with the assumption that `l` is falsified.  -/
Sat.Valuation.by_cases : ∀ {v : Sat.Valuation} {l : Sat.Literal}, (v.neg l.negate → False) → (v.neg l → False) → False
-- Lean.Elab.DefView
Lean.Elab.DefParsed.mk.sizeOf_spec : ∀ (fullHeaderRef : Lean.Syntax)
  (headerProcessedSnap : Lean.Language.SnapshotTask (Option Lean.Elab.HeaderProcessedSnapshot)),
  sizeOf { fullHeaderRef := fullHeaderRef, headerProcessedSnap := headerProcessedSnap } =
    1 + sizeOf fullHeaderRef + sizeOf headerProcessedSnap
-- Std.Http.Data.Body.Basic
/-- Selector that resolves when a chunk is available or EOF is reached.
 -/
Std.Http.Body.recvSelector : {α : Type} → [self : Std.Http.Body α] → α → Std.Async.Selector (Option Std.Http.Chunk)
-- Mathlib.Logic.Basic
and_symm_left : ∀ {α : Sort u_1} (a b : α) (p : Prop), a = b ∧ p ↔ b = a ∧ p
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioi_pred_eq_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : PredOrder α] [NoMinOrder α]
  (a : α), Finset.Ioi (Order.pred a) = Finset.Ici a
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.instPreservesFiniteProductsLocalizationQ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C)
  [W.ContainsIdentities] [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts],
  CategoryTheory.Limits.PreservesFiniteProducts W.Q
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.instInhabitedWalkingReflexivePair : Inhabited CategoryTheory.Limits.WalkingReflexivePair
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.to_nhds_mono : ∀ {α : Type ua} {u₁ u₂ : UniformSpace α}, u₁ ≤ u₂ → ∀ (a : α), nhds a ≤ nhds a
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contDiffWithinAtProp_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {s : Set E} {x : E},
  ContDiffWithinAtProp (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x
-- Batteries.Classes.Order
Std.ReflCmp.compareOfLessAndEq_of_lt_irrefl : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : DecidableEq α],
  (∀ (x : α), ¬x < x) → Std.ReflCmp fun x1 x2 => compareOfLessAndEq x1 x2
-- Mathlib.Order.Partition.Finpartition
Finpartition.instNonempty : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α}, Nonempty (Finpartition a)
-- Mathlib.RingTheory.LocalRing.Module
/-- If `M → N → P → 0` is a presentation of `P` over a local ring `(R, 𝔪, k)` with
`M` finite and `N` finite free, then injectivity of `k ⊗ M → k ⊗ N` implies that `P` is free.
 -/
Module.free_of_lTensor_residueField_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  (f : M →ₗ[R] N) (g : N →ₗ[R] P) [inst_7 : IsLocalRing R],
  Function.Surjective ⇑g →
    Function.Exact ⇑f ⇑g →
      ∀ [Module.Finite R M] [Module.Finite R N] [Module.Free R N],
        Function.Injective ⇑(LinearMap.lTensor (IsLocalRing.ResidueField R) f) → Module.Free R P
-- Init.Data.Iterators.Basic
/-- This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
with `IterM.finitelyManySteps`.
 -/
Std.Iter.TerminationMeasures.Finite.rel_of_skip : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it it' : Std.Iter β},
  it.IsPlausibleStep (Std.IterStep.skip it') → { it := it'.toIterM }.Rel { it := it.toIterM }
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : SizeOf R] [inst_10 : SizeOf A] [inst_11 : SizeOf B] [inst_12 : SizeOf ι] (toAlgHom : A →ₐ[R] B)
  (map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toAlgHom.toRingHom x ∈ ℬ i),
  sizeOf { toAlgHom := toAlgHom, map_mem := map_mem } = 1 + sizeOf toAlgHom
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] (F F_1 : Finset (α × α)) (e_F : F = F_1) {k : ℕ} (h : F.card = k) (a a_1 : α),
  a = a_1 →
    ∀ (b b_1 : α),
      b = b_1 → ∀ (i i_1 : Fin (k + 1)), i = i_1 → F.intervalGapsWithin h a b i = F_1.intervalGapsWithin ⋯ a_1 b_1 i_1
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast!.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.CategoryTheory.IsomorphismClasses
/-- `IsIsomorphic` defines a setoid.  -/
CategoryTheory.isIsomorphicSetoid : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Setoid C
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.init : Array (Array (Array ℕ)) → Lean.Elab.FixedParams.Info
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.monomial_one_dvd_monomial_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [Nontrivial R] {i j : σ →₀ ℕ},
  (MvPolynomial.monomial i) 1 ∣ (MvPolynomial.monomial j) 1 ↔ i ≤ j
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- A dependent version of `Subgroup.iSup_induction`.  -/
Subgroup.iSup_induction' : ∀ {G : Type u_2} [inst : Group G] {ι : Sort u_5} (S : ι → Subgroup G) {C : (x : G) → x ∈ ⨆ i, S i → Prop},
  (∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯) →
    C 1 ⋯ →
      (∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯) →
        ∀ {x : G} (hx : x ∈ ⨆ i, S i), C x hx
-- Lean.Data.Lsp.Diagnostics
/-- Extension: preserve semantic range of errors when truncating them for display purposes.  -/
Lean.Lsp.DiagnosticWith.fullRange? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option Lean.Lsp.Range
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.refl_target : ∀ (X : Type u_7) [inst : TopologicalSpace X], (PartialHomeomorph.refl X).target = Set.univ
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_add_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (κ : ProbabilityTheory.Kernel α β),
  (μ + ν).compProd κ = μ.compProd κ + ν.compProd κ
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_le : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), s.erase a ≤ s
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The trifunctor `(F - ⊗ F -) ⊗ F -`.  -/
CategoryTheory.MonoidalCategory.curriedTensorPrePre : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C D))
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.span_range_h_le_range_diagonal : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : DecidableEq ι],
  Submodule.span R (Set.range RootPairing.GeckConstruction.h) ≤ (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R).range
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.length_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.toList.length = m.size
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.norm_contLinear_le : ∀ {𝕜 : Type u_1} {V : Type u_3} {W : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W),
  ‖f.contLinear‖ ≤ ‖f‖
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelUnopOp_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.kernelUnopOp g).inv =
    CategoryTheory.Limits.cokernel.desc g (CategoryTheory.Limits.kernel.ι g.unop).op ⋯
-- Mathlib.InformationTheory.Hamming
Hamming.ofHamming_toHamming : ∀ {ι : Type u_2} {β : ι → Type u_3} (x : (i : ι) → β i), Hamming.ofHamming (Hamming.toHamming x) = x
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.compRight_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₂ ⟶ S₃), (h.compRight ψ).h₂ = CategoryTheory.CategoryStruct.comp h.h₂ ψ.τ₂
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.toElabInfo : Lean.Elab.TermInfo → Lean.Elab.ElabInfo
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- `Matrix.orthogonalGroup n` is the group of `n` by `n` matrices where the transpose is the
inverse.  -/
Matrix.orthogonalGroup : (n : Type u) →
  [inst : DecidableEq n] → [inst_1 : Fintype n] → (R : Type v) → [inst_2 : CommRing R] → Submonoid (Matrix n n R)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The linear equivalence between `n × n` matrices and bilinear maps on `n → R`  -/
Matrix.toLinearMap₂' : (R : Type u_1) →
  {S₁ : Type u_3} →
    {S₂ : Type u_5} →
      {N₂ : Type u_10} →
        {n : Type u_11} →
          {m : Type u_12} →
            [inst : CommSemiring R] →
              [inst_1 : AddCommMonoid N₂] →
                [inst_2 : Module R N₂] →
                  [inst_3 : Semiring S₁] →
                    [inst_4 : Semiring S₂] →
                      [inst_5 : Module S₁ N₂] →
                        [inst_6 : Module S₂ N₂] →
                          [inst_7 : SMulCommClass S₁ R N₂] →
                            [inst_8 : SMulCommClass S₂ R N₂] →
                              [inst_9 : SMulCommClass S₂ S₁ N₂] →
                                [Fintype n] →
                                  [Fintype m] →
                                    [DecidableEq n] →
                                      [DecidableEq m] → Matrix n m N₂ ≃ₗ[R] (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_right_of_gcd_eq_one : ∀ {n m k : ℕ}, n.gcd m = 1 → n.gcd (m * k) = n.gcd k
-- Mathlib.Analysis.ODE.Gronwall
gronwallBound_continuous_ε : ∀ (δ K x : ℝ), Continuous fun ε => gronwallBound δ K ε x
-- Std.Time.Format.Modifier
/-- `D`: Day of year (e.g., 189).
 -/
Std.Time.Modifier.D : Std.Time.Number → Std.Time.Modifier
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.toBaseChange_surjective : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (p : Submodule R M),
  Function.Surjective ⇑(Submodule.toBaseChange A p)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableAt.coordChangeL : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [inst_18 : MemTrivializationAtlas e]
  [inst_19 : MemTrivializationAtlas e'] [inst_20 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B}
  {x : M},
  MDiffAt f x →
    f x ∈ e.baseSet → f x ∈ e'.baseSet → (MDiffAt fun y => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))) x
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- [Stacks Tag 00I0](https://stacks.math.columbia.edu/tag/00I0) ((1)) -/
PrimeSpectrum.isClosed_of_stableUnderSpecialization_of_isConstructible : ∀ {R : Type u_4} [inst : CommRing R] {s : Set (PrimeSpectrum R)},
  StableUnderSpecialization s → Topology.IsConstructible s → IsClosed s
-- Init.Data.BitVec.Lemmas
BitVec.instIdempotentOpHOr : ∀ {n : ℕ}, Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Mathlib.Algebra.DirectSum.Ring
/-- The `Semiring` structure derived from `GSemiring A`.  -/
DirectSum.semiring : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : (i : ι) → AddCommMonoid (A i)] →
        [inst_1 : AddMonoid ι] → [DirectSum.GSemiring A] → Semiring (DirectSum ι fun i => A i)
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- `Aut F` is a fundamental group for `F`.  -/
CategoryTheory.PreGaloisCategory.instIsFundamentalGroupAutFunctorFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.PreGaloisCategory.IsFundamentalGroup F (CategoryTheory.Aut F)
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixedPoints_antitone : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α],
  Antitone fun P => MulAction.fixedPoints (↥P) α
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.tensorHomEquiv_symm_apply : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G) (f : B ⟶ A.ihom.obj C),
  (A.tensorHomEquiv B C).symm f =
    Rep.ofHom
      { toLinearMap := (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Rep.Hom.hom f).flip, isIntertwining' := ⋯ }
-- Mathlib.RingTheory.KrullDimension.Zero
PrimeSpectrum.unique_of_ringKrullDimLE_zero : {R : Type u_1} → [inst : CommSemiring R] → [Ring.KrullDimLE 0 R] → [IsLocalRing R] → Unique (PrimeSpectrum R)
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.zeroProdIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Limits.zeroProdIso X).hom = CategoryTheory.Limits.prod.snd
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.checkTypeIsProp : Lean.Expr → Lean.MetaM Unit
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsAtom.smul_finset : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G} (a : G),
  Finset.IsAtom✝ K S A → Finset.IsAtom✝ K S (a • A)
-- Mathlib.Logic.Nontrivial.Basic
exists_pair_lt : ∀ (α : Type u_3) [Nontrivial α] [inst : LinearOrder α], ∃ x y, x < y
-- Lean.Meta.Tactic.LibrarySearch
/-- Tries to solve the goal by applying a library lemma
then calling `tactic` on the resulting goals.

Typically here `tactic` is `solveByElim`.

If it successfully closes the goal, returns `none` (unless `collectAll` is true).
Otherwise, it returns `some a`, where `a : Array (List MVarId × MetavarContext)`,
with an entry for each library lemma which was successfully applied,
containing a list of the subsidiary goals, and the metavariable context after the application.
When `collectAll` is true, complete solutions (with empty remaining goals) are also included
in the array instead of returning early.

(Always succeeds, and the metavariable context stored in the monad is reverted,
unless the goal was completely solved.)

(Note that if `solveByElim` solves some but not all subsidiary goals,
this is not currently tracked.)
 -/
Lean.Meta.LibrarySearch.librarySearch : Lean.MVarId →
  (optParam (List Lean.MVarId → Lean.MetaM (List Lean.MVarId)) fun g =>
      Lean.Meta.LibrarySearch.solveByElim [] false g 6) →
    (optParam (Lean.MVarId → Lean.MetaM Bool) fun x => pure true) →
      optParam ℕ 10 →
        optParam Bool true → optParam Bool false → Lean.MetaM (Option (Array (List Lean.MVarId × Lean.MetavarContext)))
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- A def to put an `Neg` instance on a type with a `Language.ring.Structure` instance.

To be used sparingly, usually only when defining a more useful definition like,
`[Language.ring.Structure K] -> [Theory.field.Model K] -> Field K`  -/
FirstOrder.Ring.negOfRingStructure : (R : Type u_2) → [FirstOrder.Language.ring.Structure R] → Neg R
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
contDiff_infty_iff_deriv : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F}, ContDiff 𝕜 (↑⊤) f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 (↑⊤) (deriv f)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Hom.le_iff_le : ∀ {X Y : PartOrdEmb} (f : X ⟶ Y) (x₁ x₂ : ↑X),
  (CategoryTheory.ConcreteCategory.hom f) x₁ ≤ (CategoryTheory.ConcreteCategory.hom f) x₂ ↔ x₁ ≤ x₂
-- Mathlib.Geometry.Manifold.Algebra.Monoid
mdifferentiableAt_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I 1 G] {a b : G},
  (MDiffAt fun x => x + a) b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.beq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : (k : α) → BEq (β k)] [∀ (k : α), ReflBEq (β k)], m₁.Equiv m₂ → (m₁ == m₂) = true
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.fun_zero : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.Kernel.HasSubgaussianMGF (fun x => 0) 0 κ ν
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.unsat_eq_cert : Lean.Grind.CommRing.Poly → ℤ → Bool