mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Async.Basic
/-- Create a new `AsyncTask` that will run after `x` has finished.
If `x`:
- errors, return an `AsyncTask` that resolves to the error.
- succeeds, run `f` on the result of `x` and return the `AsyncTask` produced by `f`.
 -/
Std.Async.AsyncTask.bind : {α β : Type} →
  Std.Async.AsyncTask α →
    (α → Std.Async.AsyncTask β) →
      optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.AsyncTask β
-- Mathlib.Probability.ConditionalProbability
/-- Conditioning first on `s` and then on `t` results in the same measure as conditioning
on `s ∩ t`.  -/
ProbabilityTheory.cond_cond_eq_cond_inter : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {s t : Set Ω},
  MeasurableSet s →
    MeasurableSet t → ∀ (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ], μ[|s][|t] = μ[|s ∩ t]
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_smul : ∀ {n : Type u_3} {R : Type u_7} {α : Type v} [inst : SMul R α] (r : R) (A : Matrix n n α), (r • A).diag = r • A.diag
-- Mathlib.RingTheory.WittVector.Frobenius
/-- `frobeniusFun` is tautologically a polynomial function.

See also `frobenius_isPoly`.  -/
WittVector.frobeniusFun_isPoly : ∀ (p : ℕ), WittVector.IsPoly p fun R x Rcr => Rcr.frobeniusFun
-- Lean.Data.Json.Basic
Lean.Json.brecOn_5.eq : ∀ {motive_1 : Lean.Json → Sort u} {motive_2 : Array Lean.Json → Sort u}
  {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} {motive_4 : List Lean.Json → Sort u}
  {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u}
  {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u}
  (t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) (F_1 : (t : Lean.Json) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t)
  (F_3 : (t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t)
  (F_4 : (t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t)
  (F_5 : (t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t)
  (F_6 : (t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Lean.Json.below_5 t → motive_6 t),
  Lean.Json.brecOn_5 t F_1 F_2 F_3 F_4 F_5 F_6 = F_6 t (Lean.Json.brecOn_5.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.Algebra.Notation.Defs
div_ite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Div α] (a b c : α),
  (a / if P then b else c) = if P then a / b else a / c
-- Init.Data.Nat.Lemmas
Nat.mul_sub_mul_div_of_dvd : ∀ {b d a c : ℕ}, b ≠ 0 → d ≠ 0 → b ∣ a → d ∣ c → (a * d - b * c) / (b * d) = a / b - c / d
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.of_isBigO_im_re_rpow : ∀ {l : Filter ℂ},
  Filter.Tendsto Complex.re l Filter.atTop → ∀ (r : ℝ), (Complex.im =O[l] fun z => z.re ^ r) → Complex.IsExpCmpFilter l
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α},
  (m₁ ∩ m₂).getKeyD k fallback = if k ∈ m₂ then m₁.getKeyD k fallback else fallback
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_Ω : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C)
  (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω)
  (isPullback :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth)
  (uniq :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] (χ' : X ⟶ Ω),
      CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m),
  (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω = Ω
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instMulOfContinuousMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : MulZeroClass β] → [ContinuousMul β] → Mul (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.double_d_eq_zero₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (a b : ι), a ≠ i₀ → (HomologicalComplex.double f hi₀₁).d a b = 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.beq_eq_beqModel : ∀ {α : Type u} {β : Type v} {x : Ord α} [inst : BEq α] [Std.TransOrd α] [Std.LawfulBEqOrd α] [inst_3 : BEq β]
  {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β},
  m₁.WF →
    m₂.WF → Std.DTreeMap.Internal.Impl.Const.beq m₁ m₂ = Std.Internal.List.Const.beqModel m₁.toListModel m₂.toListModel
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.State.mk.sizeOf_spec : ∀ (stxTrav : Lean.Syntax.Traverser) (leadWord : String) (leadWordIdent isUngrouped mustBeGrouped : Bool)
  (stack : Array Std.Format),
  sizeOf
      { stxTrav := stxTrav, leadWord := leadWord, leadWordIdent := leadWordIdent, isUngrouped := isUngrouped,
        mustBeGrouped := mustBeGrouped, stack := stack } =
    1 + sizeOf stxTrav + sizeOf leadWord + sizeOf leadWordIdent + sizeOf isUngrouped + sizeOf mustBeGrouped +
      sizeOf stack
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.ofSet_trans_ofSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} (hs : IsOpen s) {s' : Set X} (hs' : IsOpen s'),
  (OpenPartialHomeomorph.ofSet s hs).trans (OpenPartialHomeomorph.ofSet s' hs') = OpenPartialHomeomorph.ofSet (s ∩ s') ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The natural transformation `𝟭 C ⟶ t.truncGT n` when `t` is a t-structure
on a category `C` and `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.truncGTπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) → (n : ℤ) → CategoryTheory.Functor.id C ⟶ t.truncGT n
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
/-- There are only finitely many associated primes of a finitely generated module
over a Noetherian ring.  -/
associatedPrimes.finite : ∀ (A : Type u) [inst : CommRing A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M] [IsNoetherianRing A]
  [Module.Finite A M], (associatedPrimes A M).Finite
-- Mathlib.Topology.VectorBundle.Hom
continuousWithinAt_hom_bundle : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂]
  [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] {M : Type u_8}
  [inst_22 : TopologicalSpace M] (f : M → Bundle.TotalSpace (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x) {s : Set M}
  {x₀ : M},
  ContinuousWithinAt f s x₀ ↔
    ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧
      ContinuousWithinAt
        (fun x => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
        s x₀
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.giSaturation.eq_1 : ∀ (M : Type u_1) [inst : MulOneClass M],
  Submonoid.giSaturation M =
    { choice := fun s hs => { toSubmonoid := s, mulSaturated := ⋯ }, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_univ : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.closure Set.univ = ⊤
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {X Y : CategoryTheory.Sheaf J A},
  (CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf.app X).app (Opposite.op Y) =
    CategoryTheory.Sheaf.homEquiv.symm.toIso
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) (x : ↥B),
  (H.mulMapLeftOfSupEqTop H').symm ↑x = 1 ⊗ₜ[R] x
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `analyticAt_iff_analytic_mul`

---

A function is analytic at a point iff it is analytic after multiplication
with a non-vanishing analytic function.  -/
analyticAt_iff_analytic_fun_mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝}
  {z : E}, AnalyticAt 𝕜 f z → f z ≠ 0 → (AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun i => f i * g i) z)
-- Mathlib.CategoryTheory.Action
/-- Given `G` acting on `X`, a group homomorphism `φ : G →* (X → H) ⋊ G` can be uncurried to
a functor from the action groupoid to `H`, provided that `φ g = (_, g)` for all `g`.  -/
CategoryTheory.ActionCategory.uncurry : {X : Type u} →
  {G : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        {H : Type u_3} →
          [inst_2 : Group H] →
            (F : G →* (X → H) ⋊[mulAutArrow] G) →
              (∀ (g : G), (F g).right = g) →
                CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- The continuous map that is constantly zero.  -/
ContinuousLinearMap.zero : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] → [inst_7 : Module R₂ M₂] → Zero (M₁ →SL[σ₁₂] M₂)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.tsum_comm' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α]
  [T3Space α] {f : β → γ → α},
  Summable (Function.uncurry f) →
    (∀ (b : β), Summable (f b)) →
      (∀ (c : γ), Summable fun b => f b c) → ∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_typein : ∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r] (x : α),
  ((Ordinal.typein r).toRelEmbedding x).card = Cardinal.mk { y // r y x }
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.ae_le_of_hasLaw_binomial : ∀ {Ω : Type u_2} {m : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {n : ℕ} {p : ↑unitInterval} {X : Ω → ℕ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.binomial n p) P → ∀ᵐ (ω : Ω) ∂P, X ω ≤ n
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddGroup : {α : Type u_1} → [AddGroup α] → AddGroup αᵃᵒᵖ
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'.go : List Char → ℕ
-- Mathlib.Data.Fintype.Order
Finite.ciSup_sup : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {a : α},
  (⨆ i, f i) ⊔ a = ⨆ i, f i ⊔ a
-- Mathlib.Algebra.Field.Action.ConjAct
ConjAct.distribMulAction₀ : {K : Type u_1} → [inst : DivisionRing K] → DistribMulAction (ConjAct K) K
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- A continuous linear map is zero iff its norm vanishes.  -/
ContinuousMultilinearMap.opNorm_zero_iff : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ContinuousMultilinearMap 𝕜 E G}, ‖f‖ = 0 ↔ f = 0
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} (nextIdx n : ℕ) (inner : Std.IterM m β) (nextIdx_1 n_1 : ℕ)
  (inner_1 : Std.IterM m β),
  ({ nextIdx := nextIdx, n := n, inner := inner } = { nextIdx := nextIdx_1, n := n_1, inner := inner_1 }) =
    (nextIdx = nextIdx_1 ∧ n = n_1 ∧ inner = inner_1)
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) → deriv (∏ i ∈ u, f i) x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • deriv (f i) x
-- Mathlib.Algebra.Module.SpanRank
Ideal.spanRank_map_eq_of_ringEquiv : ∀ {R S : Type u} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S) (I : Ideal R),
  Submodule.spanRank (Ideal.map f I) = Submodule.spanRank I
-- Mathlib.Tactic.ITauto
/-- Given the contents of an `And` variant, return the two conjuncts.  -/
Mathlib.Tactic.ITauto.AndKind.sides : Mathlib.Tactic.ITauto.AndKind →
  Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp × Mathlib.Tactic.ITauto.IProp
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_lt_toNNReal_iff_of_nonneg : ∀ {r p : ℝ}, 0 ≤ r → (r.toNNReal < p.toNNReal ↔ r < p)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.ne_natDegree_of_mem_eraseLead_support : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} {a : ℕ}, a ∈ f.eraseLead.support → a ≠ f.natDegree
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instDecidableEqOrdinal : DecidableEq Std.Time.Week.OfYear.Ordinal
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_smul_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {p : ℝ},
  0 ≤ p → ∀ {f : α → ε} (c : ENNReal), MeasureTheory.eLpNorm' f p (c • μ) = c ^ (1 / p) * MeasureTheory.eLpNorm' f p μ
-- Mathlib.Combinatorics.Enumerative.DyckWord
_private.Mathlib.Combinatorics.Enumerative.DyckWord.0.DyckWord.ofTree.match_1.eq_2 : ∀ (motive : BinaryTree Unit → Sort u_1) (value : Unit) (l r : BinaryTree Unit) (h_1 : Unit → motive BinaryTree.nil)
  (h_2 : (value : Unit) → (l r : BinaryTree Unit) → motive (BinaryTree.node value l r)),
  (match BinaryTree.node value l r with
    | BinaryTree.nil => h_1 ()
    | BinaryTree.node value l r => h_2 value l r) =
    h_2 value l r
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_sSup : ∀ {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)
  [RingHomClass F R S] (s : Set (Ideal R)), Ideal.map f (sSup s) = ⨆ I ∈ s, Ideal.map f I
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
IsOpen.uniqueMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {s : Set M}, IsOpen s → x ∈ s → UniqueMDiffAt[s] x
-- Init.Data.UInt.Lemmas
UInt16.lt_asymm : ∀ {a b : UInt16}, a < b → ¬b < a
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.toDerivation : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] →
                          LeftInvariantDerivation I G →
                            Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
                              (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32.congr_simp : ∀ (a a_1 : ISize), a = a_1 → ∀ (h : System.Platform.numBits = 32), a.toBitVec32 h = a_1.toBitVec32 h
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCone` commutes with `postcomposeEquivalence`  -/
CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F G : CategoryTheory.Functor J C} →
                {α : F ≅ G} →
                  {c : CategoryTheory.Limits.Cone F} →
                    H.mapCone ((CategoryTheory.Limits.Cone.postcomposeEquivalence α).functor.obj c) ≅
                      (CategoryTheory.Limits.Cone.postcomposeEquivalence
                              (CategoryTheory.Functor.isoWhiskerRight α H)).functor.obj
                        (H.mapCone c)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaMon_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] (X : CategoryTheory.Mon C),
  CategoryTheory.shrinkYonedaMon.{w, v, u}.obj X = MonCat.shrinkFunctor.{w, v, v, u} (CategoryTheory.yonedaMon.obj X)
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- The semiring topology on `PowerSeries` of a topological semiring  -/
PowerSeries.WithPiTopology.instIsTopologicalSemiring : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Semiring R] [IsTopologicalSemiring R],
  IsTopologicalSemiring (PowerSeries R)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α → ENNReal) (t : Set α), ∫⁻ (x : α) in t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.IsIntegral.nonempty : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsIntegral X], Nonempty ↥X
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_dep_iff : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.IsBasis I X → ∀ {D : Set α}, (M.contract X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.not_isNonloop_iff_closure : ∀ {α : Type u_1} {M : Matroid α} {e : α}, ¬M.IsNonloop e ↔ M.closure {e} = M.loops
-- Init.Data.String.Lemmas.Modify
String.map_map : ∀ {f g : Char → Char} {s : String}, String.map g (String.map f s) = String.map (g ∘ f) s
-- Std.Http.Data.Status
Std.Http.instBEqStatus.beq : Std.Http.Status → Std.Http.Status → Bool
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.PrelocalPredicate.mk : {X : TopCat} →
  {T : ↑X → Type u_1} →
    (pred : {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop) →
      (∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x), pred f → pred fun x => f (i x)) →
        TopCat.PrelocalPredicate T
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_X_of : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ}, 2 ≤ n → (PowerSeries.trunc n) PowerSeries.X = Polynomial.X
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.coe_ofAddEquiv_symm : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α], ⇑Matrix.ofAddEquiv.symm = ⇑Matrix.of.symm
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.isNilpotent_exp_sub_one : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {a : A}, IsNilpotent a → IsNilpotent (IsNilpotent.exp a - 1)
-- Std.Http.Protocol.H1
/-- Signals EOF on the reader's input without changing the reader state.
Used internally for flow control (e.g., after rejecting `Expect: 100-continue`).
To also transition the reader to `.closed`, follow this with `setReaderState .closed`.
 -/
Std.Http.Protocol.H1.Machine.closeReader : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X X' : C} {Y : F.PartialRightAdjointSource} (f : F.obj X' ⟶ Y.obj) (g : X ⟶ X')
  {Z : C} (h : F.partialRightAdjointObj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (F.partialRightAdjointHomEquiv.symm f) h) =
    CategoryTheory.CategoryStruct.comp
      (F.partialRightAdjointHomEquiv.symm (CategoryTheory.CategoryStruct.comp (F.map g) f)) h
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.beth_univ : Cardinal.beth Ordinal.univ.{u, v} = Cardinal.univ.{u, v}
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- Construct a matrix from an array in row-major ordering.  -/
Matrix.ofArray : {R : Type u_7} → {m n : ℕ} → (A : Array R) → A.size = m * n → Matrix (Fin m) (Fin n) R
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
CategoryTheory.expComparison_ev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  (A B : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj A) ((CategoryTheory.expComparison F A).natTrans.app B))
      ((CategoryTheory.ihom.ev (F.obj A)).app (F.obj B)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A (A ⟹ B)))
      (F.map ((CategoryTheory.ihom.ev A).app B))
-- Mathlib.Topology.Maps.Basic
/-- A surjective embedding is an `IsOpenEmbedding`.  -/
Topology.IsEmbedding.isOpenEmbedding_of_surjective : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → Function.Surjective f → Topology.IsOpenEmbedding f
-- Mathlib.Algebra.Order.Group.Indicator
Function.mulSupport_iSup : ∀ {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [inst : One M] [inst_1 : ConditionallyCompleteLattice M] [Nonempty ι]
  (f : ι → α → M), (Function.mulSupport fun x => ⨆ i, f i x) ⊆ ⋃ i, Function.mulSupport (f i)