mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isRat_mul : ∀ {α : Type u_1} [inst : Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ},
  f = HMul.hMul →
    Mathlib.Meta.NormNum.IsRat a na da →
      Mathlib.Meta.NormNum.IsRat b nb db →
        na.mul nb = (↑k).mul nc → da.mul db = k.mul dc → Mathlib.Meta.NormNum.IsRat (f a b) nc dc
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.is3Clique_triple_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {a b c : α} [inst : DecidableEq α],
  G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasStrictFDerivAt c c' x → ∀ (f : F), HasStrictFDerivAt (fun y => c y • f) (c'.smulRight f) x
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_26 : HAdd Std.Time.Hour.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The canonical isomorphism `S.cycles ≅ S.homology` when `S.f = 0`.  -/
CategoryTheory.ShortComplex.asIsoHomologyπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → S.f = 0 → [inst_2 : S.HasHomology] → S.cycles ≅ S.homology
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.matcherExt : Lean.EnvExtension (Lean.PHashMap Lean.Meta.Match.MatcherKey✝ Lean.Name)
-- Mathlib.Tactic.Widget.CommDiag
/-- Given a commutative triangle `f ≫ g = h` or `e ≡ h = f ≫ g`, return a triangle diagram.
Otherwise `none`.  -/
Mathlib.Tactic.Widget.commTriangleM? : Lean.Expr → Lean.MetaM (Option ProofWidgets.Html)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.toArray_eq_empty_iff : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], r.toArray = #[] ↔ ¬r.lower < r.upper
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.mk.sizeOf_spec : ∀ {K : Type} [kDecidableEq : DecidableEq K] [kFin : Fintype K] (k₀ k₁ : K) (Γ : K → Type) (Λ : Type) (main : Λ)
  [ΛFin : Fintype Λ] (σ : Type) (initialState : σ) [σFin : Fintype σ] [Γk₀Fin : Fintype (Γ k₀)]
  (m : Λ → Turing.TM2.Stmt Γ Λ σ),
  sizeOf
      { K := K, kDecidableEq := kDecidableEq, kFin := kFin, k₀ := k₀, k₁ := k₁, Γ := Γ, Λ := Λ, main := main,
        ΛFin := ΛFin, σ := σ, initialState := initialState, σFin := σFin, Γk₀Fin := Γk₀Fin, m := m } =
    1 + sizeOf K + sizeOf kFin + sizeOf k₀ + sizeOf k₁ + sizeOf Λ + sizeOf main + sizeOf ΛFin + sizeOf σ +
          sizeOf initialState +
        sizeOf σFin +
      sizeOf Γk₀Fin
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- The `AddSubsemigroup` generated by a set  -/
AddSubsemigroup.closure : {M : Type u_1} → [inst : Add M] → Set M → AddSubsemigroup M
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_of_succ_le : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.succ ≤ i), p.predAbove i = i.pred ⋯
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_fg_of_artinian : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [IsArtinianRing R], N.FG → IsArtinian R ↥N
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_finsuppSum : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  (f : ι →₀ N) (g : ι → N → MonoidAlgebra R M), (f.sum g).coeff = f.sum fun i n => (g i n).coeff
-- Mathlib.RingTheory.Perfection
/-- **Alias** of `Perfection`.

---

The perfection of a monoid `α`, defined to be the projective limit of `α` using the `p`-th
power maps `α → α` indexed by the natural numbers, implemented as
`{ f : ℕ → M | ∀ n, f (n + 1) ^ p = f n }`.

If `α` is a ring with characteristic `p` and `p` is prime, `Perfection α p` is also a ring.  -/
Ring.Perfection : (α : Type u₁) → [Pow α ℕ] → ℕ → Type u₁
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_mk : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  (i : HomogeneousLocalization.NumDenSameDeg 𝒜 x),
  (HomogeneousLocalization.mk i).val = Localization.mk ↑i.num ⟨↑i.den, ⋯⟩
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.T_mul : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ) (f : LaurentPolynomial R),
  LaurentPolynomial.T n * f = f * LaurentPolynomial.T n
-- Mathlib.Algebra.Order.Group.Abs
sub_lt_of_abs_sub_lt_left : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b c : G},
  |a - b| < c → b - c < a
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piScalarRightHomBil.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] (ι : Type u_4),
  TensorProduct.piScalarRightHomBil R S N ι =
    { toFun := fun n => (LinearMap.toSpanSingleton R N n).compLeft ι, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Finsupp.curryEquiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M],
  Finsupp.curryEquiv = { toFun := Finsupp.curry, invFun := Finsupp.uncurry, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.map_smul : ∀ {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) (c : R) (x : A), f (c • x) = c • f x
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
  {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω},
  MeasurableSet E → Filter.limsup (fun i => (μs i) E) L ≤ μ E → μ Eᶜ ≤ Filter.liminf (fun i => (μs i) Eᶜ) L
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars' : ∀ {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field L] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module L M] [inst_4 : Module L N] (P : RootPairing ι L M N) (K : Type u_5)
  [inst_5 : Field K] [inst_6 : Algebra K L] [inst_7 : Module K M] [inst_8 : Module K N] [inst_9 : IsScalarTower K L M]
  [inst_10 : IsScalarTower K L N] [inst_11 : P.IsBalanced] [inst_12 : P.IsValuedIn K],
  (P.restrictScalars' K).IsRootSystem
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.of_zpow : ∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α] {n : ℤ},
  (f ^ n).IsCycle → f.support ⊆ (f ^ n).support → f.IsCycle
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.mk.eq_1 : ∀ {ι : Type u_1} {A : ι → Type u_2}, GradedMonoid.mk = Sigma.mk
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.negOnePow_mul_iterateDerivativeC_nonneg : ∀ {n k i : ℕ}, i ≤ n → ∀ {x : ℝ}, 1 ≤ x → 0 ≤ (-1) ^ i * Polynomial.Chebyshev.iterateDerivativeC✝ n k x i
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_biSup_of_directedOn : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {p : ι → Prop} {K : ι → AddSubgroup G} {i : ι},
  p i →
    DirectedOn (Function.onFun (fun x1 x2 => x1 ≤ x2) K) {i | p i} →
      ∀ {x : G}, x ∈ ⨆ i, ⨆ (_ : p i), K i ↔ ∃ i, p i ∧ x ∈ K i
-- Mathlib.Algebra.Module.Defs
neg_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R) (x : M),
  -r • x = -(r • x)
-- Lean.Elab.Parallel
/-- Runs a list of MetaM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in original order.

The iterator runs in MetaM, and as it yields each result, it updates the MetaM state
to reflect the state when that particular task completed. This means the state is
threaded through the iteration in the order of the original list.

Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
Lean.Meta.MetaM.parIterWithCancel : {α : Type} → List (Lean.MetaM α) → Lean.MetaM (BaseIO PUnit.{1} × Std.IterM Lean.MetaM (Except Lean.Exception α))
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instWEqualsLocallyBijectiveEtaleSmallEtaleTopology : ∀ {S : AlgebraicGeometry.Scheme} {A : Type u'} [inst : CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1}
  {CD : A → Type u} [inst_1 : (X Y : A) → FunLike (FA X Y) (CD X) (CD Y)]
  [inst_2 : CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A]
  [(CategoryTheory.forget A).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)],
  S.smallEtaleTopology.WEqualsLocallyBijective A
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
AddMonoidAlgebra.cardinalMk_eq_lift_of_fintype : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [inst_1 : Fintype M'],
  Cardinal.mk (AddMonoidAlgebra R M') = Cardinal.lift.{v, u} (Cardinal.mk R) ^ Fintype.card M'
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesFiniteColimits F] (J : Type)
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
cot_pi_mul_contDiffWithinAt : ∀ {x : ℂ} (k : ℕ∞),
  x ∈ Complex.integerComplement →
    ContDiffWithinAt ℂ (↑k) (fun x => (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet x
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- Describes the property of a functor to "preserve sheaves".  -/
CategoryTheory.GrothendieckTopology.HasSheafCompose : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {B : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} B] →
            CategoryTheory.GrothendieckTopology C → CategoryTheory.Functor A B → Prop
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [inst_5 : Finite G]
  {H : Subgroup G},
  (IsGaloisGroup.intermediateFieldEquivSubgroup G K L).symm (OrderDual.toDual H) = FixedPoints.intermediateField ↥H
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.fold_filterMapWithPostcondition : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Do.WPMonad n ps]
  [inst_5 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Std.Iterators.PostconditionT n (Option γ)}
  {g : δ → γ → δ} {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __x ← (f b).run
          match __x with
            | some c => pure (g d c)
            | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.Iter.filterMapWithPostcondition f it) ⦃Q⦄
-- Init.Data.Fin.Lemmas
Fin.lt_add_one_iff : ∀ {n : ℕ} {k : Fin (n + 1)}, k < k + 1 ↔ k < Fin.last n
-- Std.Http.Server.Connection
Std.Http.Server.Connection.mk.injEq : ∀ {α : Type} (socket : α) (machine : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving)
  (extensions : Std.Http.Extensions) (socket_1 : α)
  (machine_1 : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving)
  (extensions_1 : Std.Http.Extensions),
  ({ socket := socket, machine := machine, extensions := extensions } =
      { socket := socket_1, machine := machine_1, extensions := extensions_1 }) =
    (socket = socket_1 ∧ machine = machine_1 ∧ extensions = extensions_1)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- `Function.eval` as a `RingHom` on the ring of `C^n` functions.  -/
ContMDiffMap.evalRingHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {R : Type u_10} →
                                      [inst_9 : CommRing R] →
                                        [inst_10 : TopologicalSpace R] →
                                          [inst_11 : ChartedSpace H' R] →
                                            [inst_12 : ContMDiffRing I' n R] → N → ContMDiffMap I I' N R n →+* R
-- Init.Data.Array.Lemmas
Array.not_mem_push_of_ne_of_not_mem : ∀ {α : Type u_1} {a y : α} {xs : Array α}, a ≠ y → a ∉ xs → a ∉ xs.push y
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_rii : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : Std.PRange.Least? α] [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α] {xs : Std.Rii α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.π.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [inst : (i : I) → Decidable (J i)],
  Profinite.NobelingProof.π C J = Profinite.NobelingProof.Proj J '' C
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Function.Bijective.sum_comp : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  {e : ι → κ}, Function.Bijective e → ∀ (g : κ → M), ∑ i, g (e i) = ∑ i, g i
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.le_op_iff : ∀ {G : Type u_2} [inst : AddGroup G] {S₁ : AddSubgroup Gᵃᵒᵖ} {S₂ : AddSubgroup G}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
isIdempotentElem_iff_quasispectrum_subset : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : Field R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : Module R A] [inst_9 : IsScalarTower R A A]
  [inst_10 : SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  p a → (IsIdempotentElem a ↔ quasispectrum R a ⊆ {0, 1})
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_add_apply : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {V V₁ : (x : M') → TangentSpace I' x},
  VectorField.mpullback I I' f (V + V₁) x = VectorField.mpullback I I' f V x + VectorField.mpullback I I' f V₁ x
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.epsilon_succ_eq_nfp : ∀ (o : Ordinal.{u_1}), (Order.succ o).epsilon = Ordinal.nfp (fun a => Ordinal.omega0 ^ a) (Order.succ o.epsilon)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
SeminormedAddCommGroup.toAddCommGroup.hcongr_2 : ∀ (E E' : Type u_8),
  E = E' →
    ∀ (self : SeminormedAddCommGroup E) (self' : SeminormedAddCommGroup E'),
      self ≍ self' → self.toAddCommGroup ≍ self'.toAddCommGroup
-- Init.Core
imp_self : ∀ {a : Prop}, a → a ↔ True
-- Init.Data.SInt.Lemmas
Int8.sub_eq_iff_eq_add : ∀ {a b c : Int8}, a - b = c ↔ a = c + b
-- Mathlib.Algebra.Group.Action.Option
Option.instVAddAssocClassOfVAdd : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [inst_2 : VAdd M N]
  [VAddAssocClass M N α], VAddAssocClass M N (Option α)
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instAddCommMonoidWithOne : {R : Type u_1} → [AddCommMonoidWithOne R] → AddCommMonoidWithOne Rᵐᵒᵖ
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.comp_lift : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  {P' : Type u_4} [inst_3 : Monoid P'] (f : P →* P') (g₁ : M →* P) (g₂ : N →* P),
  f.comp (Monoid.Coprod.lift g₁ g₂) = Monoid.Coprod.lift (f.comp g₁) (f.comp g₂)
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_append_iff : ∀ {α : Type u_1} {n m : ℕ} {β : Type u_2} {xs : Vector α (n + m)} {f : (i : ℕ) → α → i < n + m → β} {ys : Vector β n}
  {zs : Vector β m},
  xs.mapFinIdx f = ys ++ zs ↔
    ∃ ys' zs',
      xs = ys' ++ zs' ∧ (ys'.mapFinIdx fun i a h => f i a ⋯) = ys ∧ (zs'.mapFinIdx fun i a h => f (i + n) a ⋯) = zs
-- Mathlib.Analysis.Normed.Module.Convex
/-- Given a point `x` in the convex hull of `s` and a point `y` in the convex hull of `t`,
there exist points `x' ∈ s` and `y' ∈ t` at distance at least `dist x y`.  -/
convexHull_exists_dist_ge2 : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s t : Set E} {x y : E},
  x ∈ (convexHull ℝ) s → y ∈ (convexHull ℝ) t → ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.prod : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {α' : Type u_1} {β' : Type u_2}
  [inst_2 : UniformSpace α'] [inst_3 : UniformSpace β'] {e₁ : α → α'} {e₂ : β → β'},
  IsUniformInducing e₁ → IsUniformInducing e₂ → IsUniformInducing fun p => (e₁ p.1, e₂ p.2)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.eq_1 : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂), f.HasFiniteRange = f.range.FG
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.  -/
OrderAddMonoidIso.apply_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) (y : β), e (e.symm y) = y
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instHashableDSimpArgs.hash : Lean.Elab.Tactic.Grind.DSimpArgs → UInt64
-- Mathlib.Combinatorics.Matroid.Basic
/-- The ground set is nonempty  -/
Matroid.Nonempty.ground_nonempty : ∀ {α : Type u_1} {M : Matroid α} [self : M.Nonempty], M.E.Nonempty
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.coe_toCLMEquiv : ∀ {X : Type u_1} {R : Type u_3} {E : Type u_4} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : CommRing R] [inst_5 : TopologicalSpace R]
  [inst_6 : IsTopologicalRing R] [inst_7 : Module R E] [inst_8 : ContinuousSMul R E] (μ : AbstractMeasure X R E)
  (f : C(X, R)), (AbstractMeasure.toCLMEquiv μ) f = μ f
-- Mathlib.Data.String.Basic
String.head_empty : "".toList.head! = default
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instDecidableMem : {α : Type u} → {cmp : α → α → Ordering} → {t : Std.TreeSet.Raw α cmp} → {a : α} → Decidable (a ∈ t)
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.ExtTreeMap.getEntryLTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α × β → α × β
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- **Alias** of the forward direction of `linearIndependent_iff_injective_finsuppLinearCombination`. -/
LinearIndependent.finsuppLinearCombination_injective : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → Function.Injective ⇑(Finsupp.linearCombination R v)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (K : TopologicalSpace.Compacts α) (L : TopologicalSpace.Compacts β), ↑(K ×ˢ L) = ↑K ×ˢ ↑L
-- Mathlib.Data.List.Sigma
List.NodupKeys.eq_1 : ∀ {α : Type u} {β : α → Type v} (l : List (Sigma β)), l.NodupKeys = l.keys.Nodup
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given additive congruence relations `c, d` on an `AddMonoid` such that `d`
contains `c`, `d`'s quotient map induces a homomorphism from the quotient by `c` to the quotient
by `d`.  -/
AddCon.map : {M : Type u_1} → [inst : AddZeroClass M] → (c d : AddCon M) → c ≤ d → c.Quotient →+ d.Quotient
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instModule : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  {S : Type u_5} →
                    [inst_6 : Semiring S] →
                      [inst_7 : Module S M] →
                        [SMulCommClass R S M] → [SMulCommClass S A M] → Module S (Derivation R A M)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_pos'`.  -/
Right.add_pos' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b : α}, 0 < a → 0 < b → 0 < a + b
-- Mathlib.Logic.Function.Basic
Function.curry_injective : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3}, Function.Injective Function.curry