mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Defs
Ideal.add_mem_iff_right : ∀ {α : Type u} [inst : Ring α] (I : Ideal α) {a b : α}, a ∈ I → (a + b ∈ I ↔ b ∈ I)
-- Mathlib.Data.Sum.Basic
Sum.liftRel_iff : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (r : α → γ → Prop) (s : β → δ → Prop) (a : α ⊕ β)
  (a_1 : γ ⊕ δ),
  Sum.LiftRel r s a a_1 ↔
    (∃ a_2 c, r a_2 c ∧ a = Sum.inl a_2 ∧ a_1 = Sum.inl c) ∨ ∃ b d, s b d ∧ a = Sum.inr b ∧ a_1 = Sum.inr d
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkFunctor_map_germ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {F G : TopCat.Presheaf C X} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U) (f : F ⟶ G),
  CategoryTheory.CategoryStruct.comp (F.germ U x hx) ((TopCat.Presheaf.stalkFunctor C x).map f) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (G.germ U x hx)
-- Mathlib.Geometry.Manifold.Instances.Real
IccLeftChart.eq_1 : ∀ (x y : ℝ) [h : Fact (x < y)],
  IccLeftChart x y =
    { toFun := fun z => ⟨WithLp.toLp 2 fun x_1 => ↑z - x, ⋯⟩, invFun := fun z => ⟨min ((↑z).ofLp 0 + x) y, ⋯⟩,
      source := {z | ↑z < y}, target := {z | (↑z).ofLp 0 < y - x}, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯,
      right_inv' := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ }
-- Mathlib.CategoryTheory.Action.Basic
Action.hom_inv_hom_assoc : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M ≅ N) {Z : V} (h : M.V ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp f.inv.hom h) = h
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- (internal implementation) the fact that the proposed limit cone is the limit  -/
CategoryTheory.Limits.Types.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type (max v u))) →
      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.limitCone F)
-- Lean.Linter.UnusedVariables
/-- Enables or disables unused variable linter warnings in function arguments  -/
Lean.Linter.linter.unusedVariables.funArgs : Lean.Option Bool
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Compatibility with the structure morphism, for a morphism of algebras.  -/
CategoryTheory.Monad.Algebra.Hom.h : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
  (self : A.Hom B),
  CategoryTheory.CategoryStruct.comp (T.map self.f) B.a = CategoryTheory.CategoryStruct.comp A.a self.f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A subspace is less than another if and only if it is less than or equal to the second subspace
and there is a point only in the second.  -/
AffineSubspace.lt_iff_le_and_exists : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The object in `PresheafOfModules R` that is obtained from `M : Cᵒᵖ ⥤ Ab.{v}` such
that for all `X : Cᵒᵖ`, `M.obj X` is a `R.obj X` module, in such a way that the
restriction maps are semilinear. (This constructor should be used only in cases
when the preferred constructor `PresheafOfModules.mk` is not as convenient as this one.)  -/
PresheafOfModules.ofPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (M : CategoryTheory.Functor Cᵒᵖ Ab) →
        [inst_1 : (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)] →
          (∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)),
              (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
                (CategoryTheory.ConcreteCategory.hom (R.map f)) r • (CategoryTheory.ConcreteCategory.hom (M.map f)) m) →
            PresheafOfModules R
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₁_veblen : ∀ {o a : Ordinal.{u}}, a < Ordinal.veblen o a → (Ordinal.veblen o a).invVeblen₁ = o
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log(m + n)). Concatenate two trees that are ordered with respect to each other.

```
merge {1, 2} {3, 4} = {1, 2, 3, 4}
merge {3, 4} {1, 2} = precondition violation
```  -/
Ordnode.merge : {α : Type u_1} → Ordnode α → Ordnode α → Ordnode α
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of the transpose of an endomorphism coincides with its determinant.  -/
LinearMap.det_dualMap : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] (f : M →ₗ[R] M), LinearMap.det f.dualMap = LinearMap.det f
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_left_inj : ∀ {x y z : ℕ}, x ^^^ z = y ^^^ z ↔ x = y
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.smul_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] {S : Type u_3}
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S A] [inst_7 : SMulCommClass 𝕜 S A] [inst_8 : ContinuousConstSMul S A]
  [inst_9 : IsScalarTower S A A] [inst_10 : SMulCommClass S A A] (s : S) (a : DoubleCentralizer 𝕜 A),
  (s • a).toProd.2 = s • a.toProd.2
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalHorizontalCompAux'_whisker : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f f' g g' h : C}
  {η : g ⟶ h} {θ : f' ⟶ g'}
  {ηθ : CategoryTheory.MonoidalCategoryStruct.tensorObj g f' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj h g'}
  {η₁ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj g f') ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj h g')}
  {η₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorObj g f') ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f h) g'}
  {η₃ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f g) f' ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj f h) g'},
  CategoryTheory.MonoidalCategoryStruct.tensorHom η θ = ηθ →
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft f ηθ = η₁ →
      CategoryTheory.CategoryStruct.comp η₁ (CategoryTheory.MonoidalCategoryStruct.associator f h g').inv = η₂ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator f g f').hom η₂ = η₃ →
          CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η) θ = η₃
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.map_ofFixingAddSubgroupUnion.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (s t : Set α),
  SubAddAction.map_ofFixingAddSubgroupUnion M s t = { toFun := fun x => ⟨⟨↑x, ⋯⟩, ⋯⟩, map_vadd' := ⋯ }
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instAdd : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → Add (SkewMonoidAlgebra k G)
-- Init.Data.Int.Order
Int.natAbs_sub_of_nonneg_of_le : ∀ {a b : ℤ}, 0 ≤ b → b ≤ a → (a - b).natAbs = a.natAbs - b.natAbs
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsCofiltered J],
      CategoryTheory.Limits.ReflectsLimitsOfShape J F) →
    CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.isThin_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C),
  S.IsThin ↔ ∀ (c : ↑S.objs), Subsingleton ↑(S.arrows ↑c ↑c)
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Finset.isSquare_prod : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} (f : ι → M),
  (∀ c ∈ s, IsSquare (f c)) → IsSquare (∏ i ∈ s, f i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k a fallback : α} {v : β k},
  (t.insert k v).getKeyD a fallback = if cmp k a = Ordering.eq then k else t.getKeyD a fallback
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.neg_add_cancel : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R M N), -x + x = 0
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2) [inst_2 : Inhabited I]
      (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)), (↑↑l).head! = Profinite.NobelingProof.term I ho
-- Mathlib.Tactic.ToExpr
/-- Hand-written instance since `PUnit` is a `Sort` rather than a `Type`.  -/
Mathlib.instToExprPUnitOfToLevel_mathlib : [Lean.ToLevel] → Lean.ToExpr PUnit.{u + 1}
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- If `G` is `n`-colorable, then mapping the vertices of `G` produces an `n`-colorable simple
graph.  -/
SimpleGraph.Colorable.map : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ} {β : Type u_3} (f : V ↪ β) [NeZero n],
  G.Colorable n → (SimpleGraph.map (⇑f) G).Colorable n
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinder : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {P : HomotopicalAlgebra.Cylinder X} {f g : X ⟶ Y} (h : P.LeftHomotopy f g),
  ∃ P', P'.IsGood ∧ Nonempty (P'.LeftHomotopy f g)
-- Init.Data.Array.Lemmas
Array.lt_of_getElem : ∀ {α : Type u_1} {x : α} {xs : Array α} {i : ℕ} {hidx : i < xs.size}, xs[i] = x → i < xs.size
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- `pi` construction for continuous linear functions. From a family of continuous linear functions
it produces a continuous linear function into a family of topological modules.  -/
ContinuousLinearMap.pi : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] →
            {ι : Type u_4} →
              {φ : ι → Type u_5} →
                [inst_4 : (i : ι) → TopologicalSpace (φ i)] →
                  [inst_5 : (i : ι) → AddCommMonoid (φ i)] →
                    [inst_6 : (i : ι) → Module R (φ i)] → ((i : ι) → M →L[R] φ i) → M →L[R] (i : ι) → φ i
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_toSubring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  S.op.toSubring = S.toSubring.op
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- Destructor for composition  -/
PFunctor.comp.get : (P₂ : PFunctor.{uA₂, uB₂}) → (P₁ : PFunctor.{uA₁, uB₁}) → {α : Type v} → ↑(P₂.comp P₁) α → ↑P₂ (↑P₁ α)
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.mk.inj : ∀ {P : TopCat → Prop} {toTop : TopCat} {is_compact : CompactSpace ↑toTop} {is_hausdorff : T2Space ↑toTop}
  {prop : P toTop} {toTop_1 : TopCat} {is_compact_1 : CompactSpace ↑toTop_1} {is_hausdorff_1 : T2Space ↑toTop_1}
  {prop_1 : P toTop_1},
  { toTop := toTop, is_compact := is_compact, is_hausdorff := is_hausdorff, prop := prop } =
      { toTop := toTop_1, is_compact := is_compact_1, is_hausdorff := is_hausdorff_1, prop := prop_1 } →
    toTop = toTop_1
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- The canonical map from the adic completion of the product to the product of the
adic completions.  -/
AdicCompletion.pi : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {ι : Type u_6} →
        (M : ι → Type u_7) →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              AdicCompletion I ((j : ι) → M j) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I (M j)
-- Lean.Declaration
Lean.RecursorVal.kEx : Lean.RecursorVal → Bool
-- Mathlib.NumberTheory.FactorisationProperties
/-- `n : ℕ` is _deficient_ if the sum of the proper divisors of `n` is less than `n`.  -/
Nat.Deficient : ℕ → Prop
-- Mathlib.Order.UpperLower.Basic
isUpperSet_Ici : ∀ {α : Type u_1} [inst : Preorder α] (a : α), IsUpperSet (Set.Ici a)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.pair_mem_prod : ∀ {x y a b : ZFSet.{u}}, a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y
-- Mathlib.Order.Bounds.Basic
IsGLB.lowerBounds_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGLB s a → lowerBounds s = Set.Iic a
-- Init.Data.SInt.Lemmas
Int16.not_le : ∀ {n m : Int16}, ¬n ≤ m ↔ m < n
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_unitIso_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapIso i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instCharZero : ∀ (K : Type u_1) [inst : Field K] [NumberField K], CharZero (NumberField.RingOfIntegers K)
-- Batteries.Data.Random.MersenneTwister
/-- Initialization multiplier (`f`).  -/
Batteries.Random.MersenneTwister.Config.initMult : (self : Batteries.Random.MersenneTwister.Config) → BitVec self.wordSize
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndParamKind.dropped : Lean.Meta.FunIndParamKind
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.Config.mk.injEq : ∀ (wordSize stateSize : ℕ) (shiftSize : Fin stateSize) (maskBits : Fin wordSize) (xorMask : BitVec wordSize)
  (temperingShifts : ℕ × ℕ × ℕ × ℕ) (temperingMasks : BitVec wordSize × BitVec wordSize × BitVec wordSize)
  (initMult initSeed : BitVec wordSize) (wordSize_1 stateSize_1 : ℕ) (shiftSize_1 : Fin stateSize_1)
  (maskBits_1 : Fin wordSize_1) (xorMask_1 : BitVec wordSize_1) (temperingShifts_1 : ℕ × ℕ × ℕ × ℕ)
  (temperingMasks_1 : BitVec wordSize_1 × BitVec wordSize_1 × BitVec wordSize_1)
  (initMult_1 initSeed_1 : BitVec wordSize_1),
  ({ wordSize := wordSize, stateSize := stateSize, shiftSize := shiftSize, maskBits := maskBits, xorMask := xorMask,
        temperingShifts := temperingShifts, temperingMasks := temperingMasks, initMult := initMult,
        initSeed := initSeed } =
      { wordSize := wordSize_1, stateSize := stateSize_1, shiftSize := shiftSize_1, maskBits := maskBits_1,
        xorMask := xorMask_1, temperingShifts := temperingShifts_1, temperingMasks := temperingMasks_1,
        initMult := initMult_1, initSeed := initSeed_1 }) =
    (wordSize = wordSize_1 ∧
      stateSize = stateSize_1 ∧
        shiftSize ≍ shiftSize_1 ∧
          maskBits ≍ maskBits_1 ∧
            xorMask ≍ xorMask_1 ∧
              temperingShifts = temperingShifts_1 ∧
                temperingMasks ≍ temperingMasks_1 ∧ initMult ≍ initMult_1 ∧ initSeed ≍ initSeed_1)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rcc_eq_zero : ∀ {m n : ℤ} {i : ℕ}, (n + 1 - m).toNat ≤ i → (m...=n).toList[i]! = 0
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_eq_getLast!_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.max! = t.toList.getLast!
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_StateT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u_1}
  {σ α : Type u} {epost : EPred} [inst_4 : MonadExceptOf ε m] (x : StateT σ m α) (h : ε → StateT σ m α)
  (post : α → σ → Pred),
  ⦃ fun s =>
    Std.Internal.Do.wp (MonadExceptOf.tryCatch (x.run s) fun e => (h e).run s)
      (fun x =>
        match x with
        | (a, s') => post a s')
      epost ⦄
    MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.copy_eq : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (S : NonUnitalSubring R) (s : Set R) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
contMDiffAt_coordChangeL : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] [inst_16 : MemTrivializationAtlas e'] {x : B},
  x ∈ e.baseSet →
    x ∈ e'.baseSet →
      ContMDiffAt IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun b => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' b)) x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.AlgebraicGeometry.Scheme
/-- A morphism of schemes `f : X ⟶ Y` induces a local ring homomorphism from
`Y.presheaf.stalk (f x)` to `X.presheaf.stalk x` for any `x : X`.  -/
AlgebraicGeometry.Scheme.Hom.stalkMap : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (x : ↥X) → Y.presheaf.stalk (f x) ⟶ X.presheaf.stalk x
-- Mathlib.Data.Part
Part.right_dom_of_add_dom : ∀ {α : Type u_1} [inst : Add α] {a b : Part α}, (a + b).Dom → b.Dom
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.asEquivalence_unitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence] (X : C),
  F.asEquivalence.unitIso.inv.app X = F.preimage (F.objObjPreimageIso (F.obj X)).hom
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).getKey! k = if k ∈ m₂ then m₁.getKey! k else default
-- Mathlib.Data.Set.Insert
Set.insert_inter_of_mem : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∈ t → insert a s ∩ t = insert a (s ∩ t)
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_of_notMem_range : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] (f : α ↪ β) (v : α →₀ M),
  ∀ a ∉ Set.range ⇑f, (Finsupp.embDomain f v) a = 0
-- Mathlib.Order.Interval.Finset.Defs
Finset.subtype_Ico_eq : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrder α]
  (a b : Subtype p), Finset.Ico a b = Finset.subtype p (Finset.Ico ↑a ↑b)
-- Mathlib.Data.Fin.Tuple.Reflection
/-- `∀` with better defeq for `∀ x : Fin m → α, P x`.  -/
FinVec.Forall : {α : Type u_1} → {m : ℕ} → ((Fin m → α) → Prop) → Prop
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.lift_snd : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g),
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w) (CompHausLike.pullback.snd f g) = b
-- Mathlib.Algebra.Group.Defs
nsmulRec'.eq_def : ∀ {M : Type u_2} [inst : Zero M] [inst_1 : Add M] (x : ℕ) (x_1 : M),
  nsmulRec' x x_1 =
    match x, x_1 with
    | 0, x => 0
    | 1, m => m
    | k.succ.succ, m => nsmulRec' (k + 1) m + m
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.comp_addHom : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : Add α] [inst_1 : Add γ],
  Function.Periodic f c →
    ∀ (g : γ →ₙ+ α) (g_inv : α → γ), Function.RightInverse g_inv ⇑g → Function.Periodic (f ∘ ⇑g) (g_inv c)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.toAlgHom_eq_coe : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B), ↑f = ↑f
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.factorThruImageSubobject_comp_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {W : C} (k : W ⟶ X)
  (h : (CategoryTheory.Limits.imageSubobject f).Factors (CategoryTheory.CategoryStruct.comp k f)),
  (CategoryTheory.Limits.imageSubobject f).factorThru (CategoryTheory.CategoryStruct.comp k f) h =
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.factorThruImageSubobject f)
-- Mathlib.Data.Finset.Density
Finset.le_dens_sdiff : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α), t.dens - s.dens ≤ (t \ s).dens
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
/-- The principle of isolated zeros: If `f` is meromorphic at `x`, then `f` vanishes eventually in a
punctured neighborhood of `x` iff it vanishes frequently in punctured neighborhoods.

See `AnalyticAt.frequently_zero_iff_eventually_zero` for a stronger result in the analytic case.
 -/
MeromorphicAt.frequently_zero_iff_eventuallyEq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E},
  MeromorphicAt f x → ((∃ᶠ (z : 𝕜) in nhdsWithin x {x}ᶜ, f z = 0) ↔ f =ᶠ[nhdsWithin x {x}ᶜ] 0)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsAlt.self_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsAlt → ∀ (x : M), (B x) x = 0
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.iInter : ∀ {α : Type u_1} {ι : Sort u_6} {m : MeasurableSpace α} [Countable ι] {f : ι → Set α},
  (∀ (b : ι), MeasurableSet (f b)) → MeasurableSet (⋂ b, f b)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take.eq_2 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v),
  (v = u → p ≍ SimpleGraph.Walk.nil → False) → p.take 0 = SimpleGraph.Walk.nil.copy ⋯ ⋯
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- The distance on `X ⊕ Y` is a candidate  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.dist_mem_candidates : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [CompactSpace X] [CompactSpace Y]
  [Nonempty X] [Nonempty Y], (fun p => dist p.1 p.2) ∈ GromovHausdorff.candidates X Y
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.coe_eq_singleton : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, (∃ g, ↑H = {g}) ↔ H = ⊥