mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Function
Set.SurjOn.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β), Set.SurjOn f s t = (t ⊆ f '' s)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.isTable_buildTableGo : ∀ {pat : String.Slice} {table : Array ℕ} {ht₀ : 0 < table.size} {ht : table.size ≤ pat.utf8ByteSize}
  {h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i},
  String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ pat.copy.toByteArray table →
    String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ pat.copy.toByteArray
      (String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat table ht₀ ht h).toArray
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- We have that `η ^ 2 = -η - 1`.  -/
IsCyclotomicExtension.Rat.Three.eta_sq : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3), ↑⋯.unit ^ 2 = -↑⋯.unit - 1
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- This asks for an explicit `K = Frac(R)`, `L = Frac(S)`,
`R'` the integral closure of `R` in `K`, and `S' ⊆ L` the subalgebra spanned by `R'` and `S`,
to aid typeclass synthesis.

Use `not_isStronglyTranscendental_of_quasiFiniteAt` below instead.  -/
_private.Mathlib.RingTheory.ZariskisMainTheorem.0.Algebra.not_isStronglyTranscendental_of_weaklyQuasiFiniteAt_of_isDomain_aux : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_4)
  (L : Type u_5) [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra R K] [inst_6 : Algebra R L]
  [inst_7 : Algebra S L] [inst_8 : Algebra K L] [IsScalarTower R K L] [IsScalarTower R S L] [IsFractionRing R K]
  [IsFractionRing S L] {R' : Type u_6} {S' : Type u_7} [inst_13 : CommRing R'] [inst_14 : CommRing S']
  [inst_15 : Algebra R R'] [inst_16 : Algebra R' S'] [inst_17 : Algebra R S'] [inst_18 : Algebra S' L]
  [inst_19 : Algebra R' L] [IsScalarTower R' S' L] [inst_21 : Algebra R' K] [IsScalarTower R' K L]
  [inst_23 : IsScalarTower R R' S'] [FaithfulSMul S' L] [IsIntegralClosure R' R K] [IsScalarTower R R' K]
  (f : S →ₐ[R] S'),
  Function.Surjective ⇑(Algebra.TensorProduct.lift (Algebra.ofId R' S') f ⋯) →
    (algebraMap S' L).comp f.toRingHom = algebraMap S L →
      ∀ {x : S},
        (Polynomial.aeval x).Finite →
          ∀ (P : Ideal S) [inst_27 : P.IsPrime] [Algebra.WeaklyQuasiFiniteAt R P], ¬IsStronglyTranscendental R x
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instMembershipOfTransCmp : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Membership α (Std.ExtDTreeMap α β cmp)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_pow_mul_eq_self_iff : ∀ (k m : ℕ) {p : ℕ}, Nat.Prime p → (p ^ k * m / p ^ (p ^ k * m).factorization p = m ↔ m = 0 ∨ ¬p ∣ m)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.comp_id : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  (f : X →ₑ[φ] Y), f.comp (MulActionHom.id M) = f
-- Mathlib.Order.Monotone.Basic
monotone_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) ↔ Monotone f
-- Lean.Declaration
Lean.ConstantInfo.ctorInfo.sizeOf_spec : ∀ (val : Lean.ConstructorVal), sizeOf (Lean.ConstantInfo.ctorInfo val) = 1 + sizeOf val
-- Batteries.Data.List.Perm
List.Perm.idxBij_leftInverse_idxBij_symm : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Perm ys),
  Function.LeftInverse h.idxBij ⋯.idxBij
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonDeleteFile : Lean.FromJson Lean.Lsp.DeleteFile
-- Mathlib.Data.List.Sublists
List.sublists_perm_sublists' : ∀ {α : Type u} (l : List α), l.sublists.Perm l.sublists'
-- Init.Data.Vector.Range
Vector.range_eq_range' : ∀ {n : ℕ}, Vector.range n = Vector.range' 0 n
-- Mathlib.MeasureTheory.Constructions.UnitInterval
/-- `unitInterval.symm` bundled as a measurable equivalence.  -/
unitInterval.symmMeasurableEquiv : ↑unitInterval ≃ᵐ ↑unitInterval
-- Mathlib.RingTheory.LinearDisjoint
/-- In a commutative ring, if subalgebras `A` and `B` are linearly disjoint and they are
free modules, then the rank of `A ⊔ B` is equal to the product of the rank of `A` and `B`.  -/
Subalgebra.LinearDisjoint.finrank_sup_of_free : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Free R ↥A] [Module.Free R ↥B], Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥A * Module.finrank R ↥B
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_pos : ∀ (o : Ordinal.{u_1}), 0 < Cardinal.aleph o
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.exists_le_of_prod_le' : ∀ {ι : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] [MulLeftMono M]
  [MulRightStrictMono M] [MulRightMono M] {l : List ι},
  l ≠ [] → ∀ (f g : ι → M), (List.map f l).prod ≤ (List.map g l).prod → ∃ x ∈ l, f x ≤ g x
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.instMeasurableSingletonClass : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α],
  MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A linear isometry preserves the property of being orthonormal.  -/
Orthonormal.comp_linearIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] {v : ι → E},
  Orthonormal 𝕜 v → ∀ (f : E →ₗᵢ[𝕜] E'), Orthonormal 𝕜 (⇑f ∘ v)
-- Init.Data.List.MinMaxIdx
List.isSome_minIdxOn?_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α},
  (List.minIdxOn? f xs).isSome = true ↔ xs ≠ []
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.r : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput old w) → self.aig.RefVec w
-- Mathlib.Data.Setoid.Basic
Setoid.ker_apply_mk_out : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (a : α), f ⟦a⟧.out = f a
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.IsLocal.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  (P Q : CategoryTheory.ObjectProperty C) [P.IsLocal K] [Q.IsLocal K], (P ⊓ Q).IsLocal K
-- Mathlib.Data.Fintype.Lattice
Finset.mem_inf : ∀ {ι : Type u_1} {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α},
  a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.comp_id : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N), f.comp (AddMonoidHom.id M) = f
-- Init.Data.Slice.Array.Lemmas
Subarray.size_drop : ∀ {α : Type u_1} {i : ℕ} {xs : Subarray α}, Std.Slice.size (xs.drop i) = Std.Slice.size xs - i
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_gt_gt : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {R : ℝ} {f : X → ℝ},
  0 ≤ R →
    MeasureTheory.IntegrableOn f {x | R < f x} μ →
      μ {x | R < f x} ≠ 0 → μ.real {x | R < f x} * R < ∫ (x : X) in {x | R < f x}, f x ∂μ
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.toList_filter : ∀ {α : Type u} {β : α → Type v} {f : (a : α) → β a → Bool} {l : Std.DHashMap.Internal.AssocList α β},
  (Std.DHashMap.Internal.AssocList.filter f l).toList.Perm (List.filter (fun p => f p.fst p.snd) l.toList)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.summable_iff_not_tendsto_nat_atTop : ∀ {f : ℕ → NNReal}, Summable f ↔ ¬Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop
-- Mathlib.Analysis.Normed.Group.Basic
enorm_sub_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E}, ‖a - b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂'_mul : ∀ {n : Type u_11} {m : Type u_12} {m' : Type u_14} {R : Type u_16} [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] [inst_5 : Fintype m'] [inst_6 : DecidableEq m']
  (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix m m' R),
  (LinearMap.toMatrix₂' R) B * M = (LinearMap.toMatrix₂' R) (B.compl₂ (Matrix.toLin' M))
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepSets_comap_process_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)] [∀ (s : S), BorelSpace (E s)]
  [∀ (s : S), HasOuterApproxClosed (E s)] {X : (s : S) → Ω → E s} [MeasureTheory.IsProbabilityMeasure P]
  {𝒜 : Set (Set Ω)},
  (∀ A ∈ 𝒜, MeasureTheory.NullMeasurableSet A P) →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ A ∈ 𝒜,
          ∀ (I : Finset S) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ),
            ∫ (ω : Ω) in A, f fun x => X (↑x) ω ∂P = P.real A * ∫ (ω : Ω), f fun x => X (↑x) ω ∂P) →
        ProbabilityTheory.IndepSets 𝒜 {A | MeasurableSet A} P
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_bot_of_injective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S], Function.Injective ⇑f → Ideal.comap f ⊥ = ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.rightUnitor_inv_app_apply : ∀ (K : SSet) {Δ : SimplexCategoryᵒᵖ} (x : K.obj Δ),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor (K.obj Δ)).inv) x =
    (x, PUnit.unit)
-- Init.Data.Int.Lemmas
Int.ofNat_mul_negSucc : ∀ (m n : ℕ), ↑m * Int.negSucc n = -↑(m * n.succ)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_sub : ∀ {a b : Ordinal.{u_4}}, Order.IsSuccPrelimit a → b < a → Order.IsSuccLimit (a - b)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exsphere_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  (s.exsphere signs).radius = s.exradius signs
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D A} {G : CategoryTheory.Functor C A} (e : L.comp F ≅ G)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M]
  (F' : M → CategoryTheory.Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m)
  [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
  [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] [inst_8 : CategoryTheory.HasShift D M]
  [inst_9 : L.CommShift M] (n a a' : M) (ha' : n + a = a') (X : C),
  (F.shiftIso n a a' ha').hom.app (L.obj X) =
    CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.Functor.commShiftIso L n).inv.app X))
      (CategoryTheory.CategoryStruct.comp ((e' a).hom.app ((CategoryTheory.shiftFunctor C n).obj X))
        (CategoryTheory.CategoryStruct.comp ((G.shiftIso n a a' ha').hom.app X) ((e' a').inv.app X)))
-- Mathlib.Order.Category.PartOrd
/-- Constructs an equivalence between partial orders from an order isomorphism between them.  -/
PartOrd.Iso.mk : {α β : PartOrd} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.Data.Finset.Insert
Finset.mem_cons_self : ∀ {α : Type u_1} (a : α) (s : Finset α) {h : a ∉ s}, a ∈ Finset.cons a s h
-- Mathlib.CategoryTheory.Extensive
/-- A functor preserves pullback of inclusions if it preserves all pullbacks along coproduct injections.
 -/
CategoryTheory.PreservesPullbacksOfInclusions : {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.Functor C D → [CategoryTheory.Limits.HasBinaryCoproducts C] → Prop
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.instFunLike : {α : Type u_2} → {β : Type u_3} → {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → FunLike (α →+* β) α β
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns `true` if there is a theorem with exactly the same pattern and constraints is already in `s`
 -/
Lean.Meta.Grind.EMatchTheorems.containsWithSamePatterns : Lean.Meta.Grind.EMatchTheorems →
  Lean.Meta.Grind.Origin → List Lean.Expr → List Lean.Meta.Grind.EMatchTheoremConstraint → Bool
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.mk.inj : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {A : Type u_5} {inst_2 : AddMonoid A}
  {inst_3 : CategoryTheory.HasShift D A} {functor : A → CategoryTheory.Functor C D}
  {shiftIso : (n a a' : A) → n + a = a' → ((functor a').comp (CategoryTheory.shiftFunctor D n) ≅ functor a)}
  {shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A)}
  {shiftIso_add :
    ∀ (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''),
      shiftIso (m + n) a a'' ⋯ =
        (functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) ≪≫
          ((functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫
            CategoryTheory.Functor.isoWhiskerRight (shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫
              shiftIso n a a' ha'}
  {functor_1 : A → CategoryTheory.Functor C D}
  {shiftIso_1 : (n a a' : A) → n + a = a' → ((functor_1 a').comp (CategoryTheory.shiftFunctor D n) ≅ functor_1 a)}
  {shiftIso_zero_1 : ∀ (a : A), shiftIso_1 0 a a ⋯ = (functor_1 a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A)}
  {shiftIso_add_1 :
    ∀ (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''),
      shiftIso_1 (m + n) a a'' ⋯ =
        (functor_1 a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) ≪≫
          ((functor_1 a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫
            CategoryTheory.Functor.isoWhiskerRight (shiftIso_1 m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫
              shiftIso_1 n a a' ha'},
  { functor := functor, shiftIso := shiftIso, shiftIso_zero := shiftIso_zero, shiftIso_add := shiftIso_add } =
      { functor := functor_1, shiftIso := shiftIso_1, shiftIso_zero := shiftIso_zero_1,
        shiftIso_add := shiftIso_add_1 } →
    functor = functor_1 ∧ shiftIso ≍ shiftIso_1
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- A `P : AffineTargetMorphismProperty` is stable under base change if `P` holds for `Y ⟶ S`
implies that `P` holds for `X ×ₛ Y ⟶ X` with `X` and `S` affine schemes.  -/
AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange : AlgebraicGeometry.AffineTargetMorphismProperty → Prop
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.BimonObjAux_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit.hom
-- Mathlib.Topology.LocallyFinsupp
/-- Restriction commutes with taking positive parts.
 -/
Function.locallyFinsuppWithin.restrict_posPart : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U V : Set X} (D : Function.locallyFinsuppWithin U ℤ) (h : V ⊆ U),
  D⁺.restrict h = (D.restrict h)⁺
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.toLin'_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : Matrix.SpecialLinearGroup n R) (v : n → R), (Matrix.SpecialLinearGroup.toLin' A) v = (Matrix.toLin' ↑A) v
-- Mathlib.Algebra.CharP.Defs
expChar_prime : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] [Fact (Nat.Prime p)], ExpChar R p
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.toSubgraph = p.toSubgraph
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ext_coord_change_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x x' : M),
  ((extChartAt I x').symm.trans (extChartAt I x)).source = ↑I '' ((chartAt H x').symm.trans (chartAt H x)).source
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_id : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R M),
  Convexity.iConvexComb w id = Convexity.sConvexComb w
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.mk.inj : ∀ {G : Type u} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {toOpenAddSubgroup : OpenAddSubgroup G}
  {isNormal' : autoParam (↑toOpenAddSubgroup).Normal OpenNormalAddSubgroup.isNormal'._autoParam}
  {toOpenAddSubgroup_1 : OpenAddSubgroup G}
  {isNormal'_1 : autoParam (↑toOpenAddSubgroup_1).Normal OpenNormalAddSubgroup.isNormal'._autoParam},
  { toOpenAddSubgroup := toOpenAddSubgroup, isNormal' := isNormal' } =
      { toOpenAddSubgroup := toOpenAddSubgroup_1, isNormal' := isNormal'_1 } →
    toOpenAddSubgroup = toOpenAddSubgroup_1
-- Mathlib.Algebra.Algebra.Hom
AlgHom.default_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Subsingleton T] (x : S), default x = 0
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- If `m₁ s = op (m₂ s) (m₃ s)` for all `s`, then the same is true for `m₁.trim`, `m₂.trim`,
and `m₃ s`.  -/
MeasureTheory.OuterMeasure.trim_binop : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ m₃ : MeasureTheory.OuterMeasure α}
  {op : ENNReal → ENNReal → ENNReal},
  (∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)) → ∀ (s : Set α), m₁.trim s = op (m₂.trim s) (m₃.trim s)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Zero α] [inst_2 : Add α],
  Finset.nsmul = { smul := fun n s => nsmulRec n s }
-- Batteries.Tactic.Trans
Batteries.Tactic.TransRelation.implies.injEq : ∀ (name : Lean.Name) (bi : Lean.BinderInfo) (name_1 : Lean.Name) (bi_1 : Lean.BinderInfo),
  (Batteries.Tactic.TransRelation.implies name bi = Batteries.Tactic.TransRelation.implies name_1 bi_1) =
    (name = name_1 ∧ bi = bi_1)
-- Mathlib.Data.FunLike.Graded
GradedFunLike.map_mem : ∀ {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} {σ : outParam (Type u_4)} {τ : outParam (Type u_5)}
  {ι : outParam (Type u_6)} {inst : SetLike σ A} {inst_1 : SetLike τ B} {𝒜 : outParam (ι → σ)} {ℬ : outParam (ι → τ)}
  {inst_2 : FunLike F A B} [self : GradedFunLike F 𝒜 ℬ] (f : F) {i : ι} {x : A}, x ∈ 𝒜 i → f x ∈ ℬ i
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_alter_of_beq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (k == k') = true → (k' ∈ m.alter k f ↔ (f m[k]?).isSome = true)
-- Init.Data.SInt.Basic
/-- The modulo operator for word-sized signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `ISize.div`. Usually accessed via the `%`
operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `ISize.mod 5 2 = 1`
* `ISize.mod 5 (-2) = 1`
* `ISize.mod (-5) 2 = (-1)`
* `ISize.mod (-5) (-2) = (-1)`
* `ISize.mod 4 2 = 0`
* `ISize.mod 4 (-2) = 0`
* `ISize.mod 4 0 = 4`
* `ISize.mod (-4) 0 = (-4)`
 -/
ISize.mod : ISize → ISize → ISize
-- Init.Data.List.Sublist
List.mem_of_mem_drop : ∀ {α : Type u_1} {a : α} {i : ℕ} {l : List α}, a ∈ List.drop i l → a ∈ l
-- Mathlib.RepresentationTheory.Invariants
Rep.invariantsAdjunction_unit_app : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G] (x : ModuleCat k),
  (Rep.invariantsAdjunction k G).unit.app x =
    ModuleCat.ofHom (LinearMap.codRestrict ((Rep.trivialFunctor k G).obj x).ρ.invariants LinearMap.id ⋯)
-- Init.Grind.Config
Lean.Grind.GrobnerConfig.mk : Lean.Grind.NoopConfig → Lean.Grind.GrobnerConfig
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_mul_cancel_right : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  IsLocalization.mk' S (x * ↑y) y = (algebraMap R S) x
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_mono : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {s t : AffineSubspace k P₂},
  s ≤ t → AffineSubspace.comap f s ≤ AffineSubspace.comap f t
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasRightHomology]
  [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.rightHomologyMap φ =
    CategoryTheory.CategoryStruct.comp h₁.rightHomologyIso.hom
      (CategoryTheory.CategoryStruct.comp γ.φH h₂.rightHomologyIso.inv)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minEntry?_of_contains : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : BEq α] {l : List ((a : α) × β a)} {b : α},
  Std.Internal.List.containsKey b l = true → (Std.Internal.List.minEntry? l).isSome = true
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_ne_zero : ∀ {a : ENNReal}, a⁻¹ ≠ 0 ↔ a ≠ ⊤
-- Mathlib.Data.List.PeriodicityLemma
/-- The **Periodicity Lemma**, also known as the **Fine and Wilf theorem**, shows that
if word `w` of length at least `p + q - gcd p q` has two periods `p` and `q`,
then it has a period `gcd p q`.
The proof is similar to the Euclidean algorithm for computing `gcd`.
 -/
List.HasPeriod.gcd : ∀ {α : Type u_1} {w : List α} {p q : ℕ},
  w.HasPeriod p → w.HasPeriod q → p + q - p.gcd q ≤ w.length → w.HasPeriod (p.gcd q)
-- Mathlib.Order.BoundedOrder.Basic
bot_ne_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [Nontrivial α], ⊥ ≠ ⊤
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.Order.PFilter
/-- A specific witness of `pfilter.directed` when `P` has meets.  -/
Order.PFilter.inf_mem : ∀ {P : Type u_1} [inst : SemilatticeInf P] {x y : P} {F : Order.PFilter P}, x ∈ F → y ∈ F → x ⊓ y ∈ F
-- Lean.Parser.Types
Lean.Parser.FirstTokens.unknown : Lean.Parser.FirstTokens