mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- Dimension of a presentation defined as the cardinality of the generators
minus the cardinality of the relations.

Note: this definition is completely non-sensical for non-finite presentations and
even then for this to make sense, you should assume that the presentation
is a complete intersection.
 -/
Algebra.Presentation.dimension : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Presentation R S ι σ → ℕ
-- Batteries.Data.String.Lemmas
String.toString_toSubstring : ∀ (s : String), s.toRawSubstring.toString = s
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Iio : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → ∀ (b : G₀), (fun x => a * x) '' Set.Iio b = Set.Iio (a * b)
-- Mathlib.RingTheory.DividedPowers.Padic
/-- Given a divided power algebra `(B, J, δ)` and an injective ring morphism `f : A →+* B`, if `I`
is an `A`-ideal such that `I.map f = J` and such that for all `n : ℕ`, `x ∈ I`, the preimage of
`hJ.dpow n (f x)` under `f` belongs to `I`, this is the induced divided power structure on `I`.  -/
DividedPowers.ofInjective : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        (I : Ideal A) →
          (J : Ideal B) →
            (f : A →+* B) →
              Function.Injective ⇑f →
                (hJ : DividedPowers J) →
                  Ideal.map f I = J →
                    (∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)) → DividedPowers I
-- Lean.Expr
/-- Given `a b : Int`, returns `a / b`  -/
Lean.mkIntDiv : Lean.Expr → Lean.Expr → Lean.Expr
-- Std.Http.Internal.ChunkedBuffer
/-- The accumulated byte arrays.
 -/
Std.Http.Internal.ChunkedBuffer.data : Std.Http.Internal.ChunkedBuffer → Array ByteArray
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.IsZeroOrProbabilityMeasure μ
-- Mathlib.Topology.UnitInterval
/-- Helper definition for `convexComb_assoc`, giving one of the coefficients appearing
when we reassociate a convex combination.
 -/
Set.Icc.convexComb_assoc_coeff₂ : ↑unitInterval → ↑unitInterval → ↑unitInterval
-- Mathlib.Topology.Constructible
IsRetrocompact.sUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {S : Set (Set X)},
  S.Finite → (∀ s ∈ S, IsRetrocompact s) → IsRetrocompact (⋃₀ S)
-- Batteries.Recycling.MonadSatisfying.Basic
SatisfiesM_Option_eq : ∀ {α : Type u_1} {p : α → Prop} {x : Option α}, SatisfiesM p x ↔ ∀ (a : α), x = some a → p a
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.Integrable.locallyIntegrable : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X},
  MeasureTheory.Integrable f μ → MeasureTheory.LocallyIntegrable f μ
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_pow_apply_eq_rotate : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x : α) (k : ℕ),
  p.toList ((p ^ k) x) = (p.toList x).rotate k
-- Mathlib.RingTheory.Length
Module.length_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R ↥⊤ = Module.length R M
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.darts_bypass_sublist_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.darts.Sublist p.darts
-- Mathlib.Algebra.Group.Finsupp
Finsupp.singleAddHom_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (b : M), (Finsupp.singleAddHom a) b = fun₀ | a => b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.pi_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I)
  {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right}
  (hd : CategoryTheory.Limits.IsLimit d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.sndPiMapOfIsLimit c hd)
-- Lean.Meta.Tactic.Cases
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.withNewEqs.loop : {α : Type} →
  Array Lean.Expr →
    Array Lean.Expr →
      (Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) → ℕ → Array Lean.Expr → Array Lean.Expr → Lean.MetaM α
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- If the projection maps in the cone are epimorphic and the cone is limiting, then
`LightProfinite.Extend.functor` is initial.
 -/
LightProfinite.Extend.functor_initial : ∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)],
  (LightProfinite.Extend.functor c).Initial
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.CommRingCat.Colimits.descFunLift.match_1.eq_5 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (motive : CommRingCat.Colimits.Prequotient F → Sort u_2) (x y : CommRingCat.Colimits.Prequotient F)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (CommRingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive CommRingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive CommRingCat.Colimits.Prequotient.one)
  (h_4 : (x : CommRingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match x.add y with
    | CommRingCat.Colimits.Prequotient.of j x => h_1 j x
    | CommRingCat.Colimits.Prequotient.zero => h_2 ()
    | CommRingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_5 x y
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.familyOfElementsOfSection.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) {U : Cᵒᵖ} (s : F.obj U) (x : C) (i : x ⟶ Opposite.unop U)
  (hi : (G.sieveOfSection s).arrows i),
  G.familyOfElementsOfSection s i hi = ⟨(CategoryTheory.ConcreteCategory.hom (F.map i.op)) s, hi⟩
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_of_indep_of_le : ∀ {Ω : Type u_1} {m₁ m₂ m₃ m₄ _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.Indep m₁ m₂ μ → m₃ ≤ m₁ → m₄ ≤ m₂ → ProbabilityTheory.Indep m₃ m₄ μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) (u : R),
  W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_len_le : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  A.EqId ↔ (Opposite.unop Δ).len ≤ (Opposite.unop A.fst).len
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- There is an explicit change of variables of a `WeierstrassCurve` to
a normal form of characteristic ≠ 2, provided that 2 is invertible in the ring.  -/
WeierstrassCurve.toCharNeTwoNF : {R : Type u_1} → [inst : CommRing R] → WeierstrassCurve R → [Invertible 2] → WeierstrassCurve.VariableChange R
-- Init.Prelude
/-- The completely homogeneous version of `Pow` where the exponent has the same type as the base.
The purpose of this class is that it provides a default `Pow` instance,
which can be used to specialize the exponent to have the same type as the base's type during elaboration.
This is to say, a type should provide an instance for this class in case `x ^ y` should be elaborated
with both `x` and `y` having the same type.

For example, the `Float` type provides an instance of this class, which causes expressions
such as `(2.2 ^ 2.2 : Float)` to elaborate.  -/
HomogeneousPow : Type u → Type u
-- Mathlib.RingTheory.Etale.QuasiFinite
/-- A variant of `Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver` that also gives you
control on the primes in the integral closure.  -/
Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [p.IsPrime] (q : Ideal S) [inst_4 : q.IsPrime] [q.LiesOver p] [Algebra.FiniteType R S] [Algebra.QuasiFiniteAt R q],
  ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hs⟩ ∈ q'
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.summable_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} {s : Set β}, Summable (f ∘ Subtype.val) → (Summable (f ∘ Subtype.val) ↔ Summable f)
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.brecOn : ∀ {α : Type u} {β : α → Type v} {motive : (a : Std.DTreeMap.Internal.Impl α β) → a.Balanced → Prop}
  {a : Std.DTreeMap.Internal.Impl α β} (t : a.Balanced),
  (∀ (a : Std.DTreeMap.Internal.Impl α β) (t : a.Balanced), Std.DTreeMap.Internal.Impl.Balanced.below t → motive a t) →
    motive a t
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.CheckResult.propagated.sizeOf_spec : sizeOf Lean.Meta.Grind.CheckResult.propagated = 1
-- Mathlib.Order.Filter.CountableInter
/-- `countableGenerate g` is the greatest `countableInterFilter` containing `g`.  -/
Filter.countableGenerate_isGreatest : ∀ {α : Type u_2} (g : Set (Set α)), IsGreatest {f | CountableInterFilter f ∧ g ⊆ f.sets} (Filter.countableGenerate g)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_eq_minKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.minKey! = t.minKeyD default
-- Mathlib.LinearAlgebra.RootSystem.Chain
/-- Note that it is often more convenient to use `RootPairing.root_add_zsmul_mem_range_iff` than
to invoke this lemma directly.  -/
RootPairing.setOfPred_root_add_zsmul_eq_Icc_of_linearIndependent : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : CommRing R] [CharZero R] [IsDomain R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∃ q ≤ 0, ∃ p ≥ 0, {z | P.root j + z • P.root i ∈ Set.range ⇑P.root} = Set.Icc q p
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
Subgroup.normalCore_isClosed : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (H : Subgroup G),
  IsClosed ↑H → IsClosed ↑H.normalCore
-- Mathlib.Data.Set.Function
Set.mapsTo_iff_subset_preimage : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t ↔ s ⊆ f ⁻¹' t
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.const_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {d : 𝕜 → 𝔸} {d' : 𝔸} (c : 𝔸),
  HasStrictDerivAt d d' x → HasStrictDerivAt (fun y => c * d y) (c * d') x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey! k = default
-- Mathlib.NumberTheory.AbelSummation
/-- A version of `sum_mul_eq_sub_integral_mul` where the endpoint is a `Nat`.  -/
sum_mul_eq_sub_integral_mul' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (m : ℕ),
  (∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t) →
    MeasureTheory.IntegrableOn (deriv f) (Set.Icc 0 ↑m) MeasureTheory.volume →
      ∑ k ∈ Finset.Icc 0 m, f ↑k * c k =
        f ↑m * ∑ k ∈ Finset.Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑m, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey! k = m₁.getKey! k
-- Mathlib.Probability.Density
ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf' : ∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : AddGroup G]
  {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SigmaFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ],
  MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ) →
    MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ) →
      ProbabilityTheory.IndepFun X Y ℙ →
        MeasureTheory.pdf (X + Y) ℙ μ =ᵐ[μ]
          MeasureTheory.lconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.scalar` as an `AlgHom`.  -/
Matrix.scalarAlgHom : (n : Type u_3) →
  (R : Type u_7) →
    {α : Type u_11} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : CommSemiring R] → [inst_3 : Semiring α] → [inst_4 : Algebra R α] → α →ₐ[R] Matrix n n α
-- Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Complex.meromorphic_digamma : Meromorphic Complex.digamma
-- Init.Control.Lawful.Instances
ReaderT.run_seq : ∀ {m : Type u → Type u_1} {ρ α β : Type u} [inst : Monad m] (f : ReaderT ρ m (α → β)) (x : ReaderT ρ m α) (ctx : ρ),
  (f <*> x).run ctx = f.run ctx <*> x.run ctx
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.inclusion.congr_simp : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖)
  (x x_1 : RestrictedProduct (fun i => R i) (fun i => A i) 𝓖),
  x = x_1 → RestrictedProduct.inclusion R A h x = RestrictedProduct.inclusion R A h x_1
-- Mathlib.Data.Finmap
Finmap.insert_singleton_eq : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b b' : β a},
  Finmap.insert a b (Finmap.singleton a b') = Finmap.singleton a b
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- If every `x ∈ s` has a neighbourhood within `s` on which `b ↦ ∑' i, f i b`
converges uniformly, then the sum converges locally uniformly. Note that this is not a tautology,
and the converse is only true if the domain is locally compact.  -/
summableLocallyUniformlyOn_of_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, SummableUniformlyOn f t) → SummableLocallyUniformlyOn f s
-- Init.Prelude
Nat.ble_eq_true_of_le : ∀ {n m : ℕ}, n ≤ m → n.ble m = true
-- Mathlib.Computability.StateTransition
StateTransition.reaches_total : ∀ {σ : Type u_1} {f : σ → Option σ} {a b c : σ},
  StateTransition.Reaches f a b →
    StateTransition.Reaches f a c → StateTransition.Reaches f b c ∨ StateTransition.Reaches f c b
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensor_associator_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z Z' : C}
  (h : Z ⟶ Z'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h)
      (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Y) h))
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffAt.coordChange : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {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] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'] {f : M → B} {g : M → F} {x : M},
  ContMDiffAt IM IB n f x →
    ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n g x →
      f x ∈ e.baseSet →
        f x ∈ e'.baseSet → ContMDiffAt IM (modelWithCornersSelf 𝕜 F) n (fun y => e.coordChange e' (f y) (g y)) x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.compare_get_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} (h' : k ∈ t), cmp (t.get k h') k = Ordering.eq
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_insert : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α},
  G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, a ≠ b → G.Adj a b
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.IsColimit.fac_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F}
  (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.inj i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) h) =
    CategoryTheory.CategoryStruct.comp (f i) h
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_eval_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (r s : R),
  Polynomial.eval (s * r) (p.scaleRoots s) = s ^ p.natDegree * Polynomial.eval r p
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.denote_go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ)
  (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (idx : ℕ) (hidx1 : idx < w),
  curr ≤ idx →
    ⟦assign,
        { aig := (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig,
          ref := (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).vec.get idx hidx1 }⟧ =
      if ⟦assign, { aig := aig, ref := discr }⟧ = true then ⟦assign, { aig := aig, ref := lhs.get idx hidx1 }⟧
      else ⟦assign, { aig := aig, ref := rhs.get idx hidx1 }⟧
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instIntCast : {R : Type u} → [inst : Ring R] → IntCast (Polynomial R)
-- Mathlib.MeasureTheory.Measure.Prod
AEMeasurable.comp_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : β → γ},
  AEMeasurable f ν → AEMeasurable (fun z => f z.2) (μ.prod ν)
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkOrCached_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (idx : ℕ) (aig : Std.Sat.AIG α) (input : aig.BinaryInput)
  {h : idx < aig.decls.size} {h2 : idx < (aig.mkOrCached input).aig.decls.size},
  (aig.mkOrCached input).aig.decls[idx] = aig.decls[idx]
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
CochainComplex.ConnectData.homologyIsoNeg.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n : ℕ) [inst_2 : NeZero n]
  (m : ℤ) (hm : m = -↑(n + 1)) [inst_3 : HomologicalComplex.HasHomology h.cochainComplex m]
  [inst_4 : HomologicalComplex.HasHomology K n], h.homologyIsoNeg n m hm = h.homologyIsoNeg n m hm
-- Init.Data.BitVec.Lemmas
/-- When the `(i+1)`th bit of `x` is false,
keeping the lower `(i + 1)` bits of `x` equals keeping the lower `i` bits.
 -/
BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false : ∀ {w : ℕ} {x : BitVec w} {i : ℕ},
  x.getLsbD i = false → BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x)
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processSepBy1 : Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Mathlib.Topology.Algebra.Order.Group
ContinuousOn.abs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G} {s : Set X},
  ContinuousOn f s → ContinuousOn (fun x => |f x|) s
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The **valuative criterion** for universally closed morphisms.  -/
AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion : @AlgebraicGeometry.UniversallyClosed = AlgebraicGeometry.ValuativeCriterion.Existence ⊓ @AlgebraicGeometry.QuasiCompact
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.get?.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : none = none → motive none)
  (h_2 : (p : (a : α) × β a) → none = some p → motive (some p)),
  (match h : none with
    | none => h_1 h
    | some p => h_2 p h) =
    h_1 ⋯
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.instLawfulMonadLiftBindFunctionFlipForallBindOfLawfulMonad : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m],
  Std.Internal.LawfulMonadLiftBindFunction fun x x_1 => flip bind
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f = g` on some neighbourhood of `x`,
then `f` is a submersion at `x` if and only if `g` is a submersion at `x`.  -/
Manifold.IsSubmersionAtOfComplement.congr_iff_of_eventuallyEq : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞}
  {f g : M → N} {x : M},
  f =ᶠ[nhds x] g → (Manifold.IsSubmersionAtOfComplement F I J n f x ↔ Manifold.IsSubmersionAtOfComplement F I J n g x)
-- Lean.LibrarySuggestions.Basic
/-- A random premise selection algorithm, provided solely for testing purposes.  -/
Lean.LibrarySuggestions.random : optParam StdGen { s1 := 37, s2 := 59 } → Lean.LibrarySuggestions.Selector
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.instInhabitedComp.default : Mathlib.Tactic.Linarith.Comp
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsMinor.antisymm : ∀ {α : Type u_1} {M N : Matroid α}, N ≤m M → M ≤m N → N = M