mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_dvd : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {x : R}, p ∣ q → Polynomial.eval x p ∣ Polynomial.eval x q
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.sUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {S : Set (Set X)},
  S.Finite → (∀ s ∈ S, Topology.IsLocallyConstructible s) → Topology.IsLocallyConstructible (⋃₀ S)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.contSupp.match_1.eq_1 : ∀ (motive : Turing.PartrecToTM2.Cont' → Sort u_1) (fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont')
  (h_1 : (fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.cons₁ fs k))
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive k.cons₂)
  (h_3 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.comp f k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.fix f k))
  (h_5 : Unit → motive Turing.PartrecToTM2.Cont'.halt),
  (match Turing.PartrecToTM2.Cont'.cons₁ fs k with
    | Turing.PartrecToTM2.Cont'.cons₁ fs k => h_1 fs k
    | k.cons₂ => h_2 k
    | Turing.PartrecToTM2.Cont'.comp f k => h_3 f k
    | Turing.PartrecToTM2.Cont'.fix f k => h_4 f k
    | Turing.PartrecToTM2.Cont'.halt => h_5 ()) =
    h_1 fs k
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Diagnostics.mk : Lean.PHashMap Lean.Meta.Origin ℕ →
  Lean.PHashMap Lean.Meta.Origin ℕ →
    Lean.PHashMap Lean.Name ℕ → Lean.PArray Lean.Meta.SimpTheorem → Lean.Meta.Simp.Diagnostics
-- Mathlib.Order.Filter.Ker
Filter.ker_eq_univ : ∀ {α : Type u_2} {f : Filter α}, f.ker = Set.univ ↔ f = ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_filterMap!_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.filterMap! f t) k =
        (Std.DTreeMap.Internal.Impl.Const.get? t k).bind fun x => f k' x
-- Mathlib.Algebra.Notation.Prod
Prod.fst_div : ∀ {G : Type u_8} {H : Type u_9} [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).1 = a.1 / b.1
-- Mathlib.Order.KrullDimension
Order.length_le_coheight : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {p : LTSeries α}, x ≤ RelSeries.head p → ↑p.length ≤ Order.coheight x
-- Batteries.Data.Fin.Coding
Fin.decodeFun.eq_2 : ∀ {n : ℕ} (m k : ℕ) (hk : k < n ^ (m + 1)),
  Fin.decodeFun ⟨k, hk⟩ = fun x =>
    match x with
    | ⟨0, ⋯⟩ => ⟨k % n, ⋯⟩
    | ⟨i.succ, hi⟩ =>
      have h := ⋯;
      Fin.decodeFun ⟨k / n, h⟩ ⟨i, ⋯⟩
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Simproc : Type
-- Init.Data.Option.Lemmas
Option.max_join_left : ∀ {α : Type u_1} [inst : Max α] {o : Option (Option α)} {o' : Option α}, o.join ⊔ o' = (o ⊔ some o').get ⋯
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.category_comp_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C)
  {x x_1 Z : CategoryTheory.Kleisli T} (f : x.Hom x_1) (g : x_1.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).of =
    CategoryTheory.CategoryStruct.comp f.of (CategoryTheory.CategoryStruct.comp (T.map g.of) (T.μ.app Z.of))
-- Mathlib.FieldTheory.IsPerfectClosure
pNilradical_eq_bot : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ}, ¬1 < p → pNilradical R p = ⊥
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionTrans : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] {i j : 𝒰.I₀} (f : i ⟶ j),
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.Cover.trans 𝒰 f)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer.eq_1 : ∀ (S : Type u) [inst : Semiring S], ascPochhammer S 0 = 1
-- Mathlib.Order.TypeTags
WithBot.instRepr : {α : Type u_1} → [Repr α] → Repr (WithBot α)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ≅ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.inv)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.hom) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
-- Lean.CoreM
/-- If `t` has not finished yet, waits for it under an `Elab.block` trace node. Returns `t`'s result.
 -/
Lean.traceBlock : {α : Type} → String → Task α → Lean.CoreM α
-- Mathlib.Order.Filter.IndicatorFunction
Antitone.indicator_eventuallyEq_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Preorder ι] [inst_1 : Zero β] (s : ι → Set α),
  Antitone s → ∀ (f : α → β) (a : α), (fun i => (s i).indicator f a) =ᶠ[Filter.atTop] fun x => (⋂ i, s i).indicator f a
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Formula for `completedSinZeta` as a Dirichlet series in the convergence range
(first version, with sum over `ℤ`).  -/
HurwitzZeta.hasSum_int_completedSinZeta : ∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum
      (fun n => (s + 1).Gammaℝ * -Complex.I * ↑n.sign * Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2)
      (HurwitzZeta.completedSinZeta (↑a) s)
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- `RootPairing.flip` as an equivalence.  -/
RootPairing.flipEquiv : (ι : Type u_1) →
  (R : Type u_2) →
    (M : Type u_3) →
      (N : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R N M ≃ RootPairing ι R M N
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.NatTrans.congr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (h : X = Y),
  α.app X =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom h))
      (CategoryTheory.CategoryStruct.comp (α.app Y) (G.map (CategoryTheory.eqToHom ⋯)))
-- Mathlib.Topology.Separation.Basic
Continuous.isOpen_mulSupport : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T1Space X] [inst_2 : One X] [inst_3 : TopologicalSpace Y]
  {f : Y → X}, Continuous f → IsOpen (Function.mulSupport f)
-- Aesop.Options.Public
/-- The transparency used by the `assumption` builtin rule. The rule applies a
hypothesis `h : T` if `T` is defeq to the goal's target at the given
transparency.
 -/
Aesop.Options.assumptionTransparency : Aesop.Options → Lean.Meta.TransparencyMode
-- Std.Http.Server.Handler
/-- A stateless HTTP handler.
 -/
Std.Http.Server.StatelessHandler : Type
-- Lean.Parser.Do
/-- `return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.

`return` not followed by a term starting on the same line is equivalent to `return ()`.
 -/
Lean.Parser.Term.doReturn : Lean.Parser.Parser
-- Mathlib.ModelTheory.Fraisse
/-- A class `K` has the joint embedding property when for every `M`, `N` in `K`, there is another
structure in `K` into which both `M` and `N` embed.  -/
FirstOrder.Language.JointEmbedding : {L : FirstOrder.Language} → Set (CategoryTheory.Bundled L.Structure) → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams : Lean.ToJson Lean.Lsp.CallHierarchyIncomingCallsParams
-- Init.Data.Float.Model.Float32
Float32.Model.mk.injEq : ∀ (toBits : UInt32) (valid : Float.Model.Format.binary32.Valid toBits.toBitVec) (toBits_1 : UInt32)
  (valid_1 : Float.Model.Format.binary32.Valid toBits_1.toBitVec),
  ({ toBits := toBits, valid := valid } = { toBits := toBits_1, valid := valid_1 }) = (toBits = toBits_1)
-- Lean.Data.Json.Basic
Lean.Json.arr.injEq : ∀ (elems elems_1 : Array Lean.Json), (Lean.Json.arr elems = Lean.Json.arr elems_1) = (elems = elems_1)
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.mk.sizeOf_spec : ∀ (toInductiveVal : Lean.InductiveVal) (lparams : List Lean.Level) (params : Array Lean.Expr)
  (compFields : Array Lean.Name) (compFieldVars indices : Array Lean.Expr) (val : Lean.Expr),
  sizeOf
      { toInductiveVal := toInductiveVal, lparams := lparams, params := params, compFields := compFields,
        compFieldVars := compFieldVars, indices := indices, val := val } =
    1 + sizeOf toInductiveVal + sizeOf lparams + sizeOf params + sizeOf compFields + sizeOf compFieldVars +
        sizeOf indices +
      sizeOf val
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_insertIfNew_le : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insertIfNew k v).size ≤ m.size + 1
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} [inst_1 : SizeOf C]
  (retraction : Y ⟶ X)
  (id :
    autoParam (CategoryTheory.CategoryStruct.comp f retraction = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.SplitMono.id._autoParam),
  sizeOf { retraction := retraction, id := id } = 1 + sizeOf retraction + sizeOf id
-- Mathlib.Logic.Function.Iterate
Function.comp_iterate_pred_of_pos : ∀ {α : Type u} (f : α → α) {n : ℕ}, 0 < n → f ∘ f^[n.pred] = f^[n]
-- Aesop.Util.UnionFind
_private.Aesop.Util.UnionFind.0.Aesop.UnionFind.mergeUnsafe : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → α → α → Aesop.UnionFind α → Aesop.UnionFind α
-- Mathlib.Topology.ContinuousOn
ContinuousOn.uncurry_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β → γ} {sα : Set α} {sβ : Set β},
  ∀ b ∈ sβ, ContinuousOn (Function.uncurry f) (sα ×ˢ sβ) → ContinuousOn (fun a => f a b) sα
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.toPiNatEquiv_symm_apply : ∀ {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) (self : Metric.PiNatEmbed X Y f),
  (Metric.PiNatEmbed.toPiNatEquiv X Y f).symm self = self.ofPiNat
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.compare_minKey?_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {km kmm : α} (hkm : t.minKey? = some km),
  (Std.ExtDTreeMap.Const.modify t k f).minKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.mk.sizeOf_spec : ∀ (changesBefore changesAfter : Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag✝),
  sizeOf { changesBefore := changesBefore, changesAfter := changesAfter } =
    1 + sizeOf changesBefore + sizeOf changesAfter
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t ≠ ∅}, (cmp (t.maxKey he) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure_eq_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G}, AddSubgroup.normalClosure s = ⨅ N, ⨅ (_ : N.Normal), ⨅ (_ : s ⊆ ↑N), N
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerLeft_left_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f))
      (CategoryTheory.Limits.pullback.fst R.hom T.hom) =
    CategoryTheory.Limits.pullback.fst R.hom S.hom
-- Aesop.Script.Step
Aesop.Script.Step.mk.injEq : ∀ (preState : Lean.Meta.SavedState) (preGoal : Lean.MVarId) (tactic : Aesop.Script.Tactic)
  (postState : Lean.Meta.SavedState) (postGoals : Array Aesop.GoalWithMVars) (preState_1 : Lean.Meta.SavedState)
  (preGoal_1 : Lean.MVarId) (tactic_1 : Aesop.Script.Tactic) (postState_1 : Lean.Meta.SavedState)
  (postGoals_1 : Array Aesop.GoalWithMVars),
  ({ preState := preState, preGoal := preGoal, tactic := tactic, postState := postState, postGoals := postGoals } =
      { preState := preState_1, preGoal := preGoal_1, tactic := tactic_1, postState := postState_1,
        postGoals := postGoals_1 }) =
    (preState = preState_1 ∧
      preGoal = preGoal_1 ∧ tactic = tactic_1 ∧ postState = postState_1 ∧ postGoals = postGoals_1)
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.id_compMultilinearMap : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂), LinearMap.id.compMultilinearMap f = f
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- Largest `b i`  -/
AkraBazziRecurrence.max_bi : {α : Type u_1} → [Finite α] → [Nonempty α] → (α → ℝ) → α
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instSubsingleton : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [∀ (i : m) (j : n), Subsingleton (α i j)],
  Subsingleton (DMatrix m n α)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRocSlice : {α : Type u} →
  [inst : Ord α] →
    Std.Roc.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RocSlice α)
-- Mathlib.CategoryTheory.WithTerminal.FinCategory
CategoryTheory.WithInitial.instFinCategory : (C : Type u) →
  [inst : CategoryTheory.SmallCategory C] →
    [CategoryTheory.FinCategory C] → CategoryTheory.FinCategory (CategoryTheory.WithInitial C)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map' : ∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : Monoid M]
  [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] {f g : Ω → M},
  Measurable f →
    Measurable g →
      MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ) →
        MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g μ) →
          ProbabilityTheory.IndepFun f g μ →
            MeasureTheory.Measure.map (f * g) μ = (MeasureTheory.Measure.map f μ).mconv (MeasureTheory.Measure.map g μ)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.edist_toLp_single_same : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b₁ b₂ : β i),
  edist (WithLp.toLp p (Pi.single i b₁)) (WithLp.toLp p (Pi.single i b₂)) = edist b₁ b₂
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_add : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {x : R},
  Polynomial.eval x (p + q) = Polynomial.eval x p + Polynomial.eval x q
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instZero : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] → [inst_6 : TopologicalSpace N] → Zero (M [⋀^ι]→L[R] N)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.toRightDerivedZero_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X : C} (I : CategoryTheory.InjectiveResolution X)
  (F : CategoryTheory.Functor C D) [inst_5 : F.Additive],
  F.toRightDerivedZero.app X =
    CategoryTheory.CategoryStruct.comp (I.toRightDerivedZero' F)
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.isoHomologyπ₀ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)).hom
        (I.isoRightDerivedObj F 0).inv)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inl_inl_pushoutAssoc_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inl
          (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
        (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) =
    CategoryTheory.Limits.pushout.inl g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
stronglyMeasurable_of_stronglyMeasurable_union_cover : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β} (s t : Set α),
  MeasurableSet s →
    MeasurableSet t →
      Set.univ ⊆ s ∪ t →
        (MeasureTheory.StronglyMeasurable fun a => f ↑a) →
          (MeasureTheory.StronglyMeasurable fun a => f ↑a) → MeasureTheory.StronglyMeasurable f
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmaKey.isPrivate : Lean.Meta.AuxLemmaKey → Bool
-- Mathlib.RingTheory.Localization.Defs
/-- If we localise a ring `R` at a submonoid `M` made of regular elements, then `r / m : R[1/M]` is
regular iff `r : R` is.  -/
IsLocalization.isRegular_mk' : ∀ {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],
  (∀ m ∈ M, IsRegular m) → ∀ {r : R} {m : ↥M}, IsRegular (IsLocalization.mk' S r m) ↔ IsRegular r
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.nthHomSeq_add : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r s : R),
  PadicInt.nthHomSeq f_compat (r + s) ≈ PadicInt.nthHomSeq f_compat r + PadicInt.nthHomSeq f_compat s
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.induce_connectedComponent : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph},
  M.IsMatching → ∀ (c : G.ConnectedComponent), (M.induce (M.verts ∩ c.supp)).IsMatching
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.ofFun_toFun : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : UniformOnFun α β 𝔖),
  (UniformOnFun.ofFun 𝔖) ((UniformOnFun.toFun 𝔖) f) = f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.Limits.pullback.snd f g) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g)
-- Mathlib.Topology.Connected.Basic
/-- Given a set `F` in a topological space `α` and a point `x : α`, the connected
component of `x` in `F` is the connected component of `x` in the subtype `F` seen as
a set in `α`. This definition does not make sense if `x` is not in `F` so we return the
empty set in this case.  -/
connectedComponentIn : {α : Type u} → [TopologicalSpace α] → Set α → α → Set α
-- Mathlib.Data.Rat.Lemmas
Rat.substr_num_den' : ∀ (q r : ℚ), (q - r).num * ↑q.den * ↑r.den = (q.num * ↑r.den - r.num * ↑q.den) * ↑(q - r).den
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β]
  [inst_4 : Max γ] [inst_5 : Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β),
  f.comp g = { toSupHom := f.comp g.toSupHom, map_bot' := ⋯ }
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_univ : ∀ {𝕜 : 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'}
  {V : (x : M') → TangentSpace I' x}, VectorField.mpullbackWithin I I' f V Set.univ = VectorField.mpullback I I' f V
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_bot_right_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter α}, Filter.Tendsto f l ⊥ ↔ l = ⊥
-- Batteries.Data.String.Lemmas
String.utf8ByteSize_mk : ∀ (cs : List Char), (String.ofList cs).utf8ByteSize = String.utf8Len cs
-- Mathlib.Algebra.Group.Pointwise.Finset.Density
Finset.dens_vadd_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β]
  [inst_3 : Fintype β] (a : α) (s : Finset β), (a +ᵥ s).dens = s.dens
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- If the sequence already terminated at position `n + 1`, nothing gets squashed.  -/
GenContFract.squashSeq_eq_self_of_terminated : ∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GenContFract.Pair K)} [inst : DivisionRing K],
  s.TerminatedAt (n + 1) → GenContFract.squashSeq s n = s
-- Mathlib.Algebra.Order.Floor.Defs
Int.floor_le : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), ↑⌊a⌋ ≤ a
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mk'.eq_1 : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 ∈ carrier)
  (add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier) (neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier)
  (mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier)
  (mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier),
  TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right =
    { ringCon := { r := fun x y => x - y ∈ carrier, iseqv := ⋯, mul' := ⋯, add' := ⋯ } }
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential in a Banach algebra `𝔸` over a normed field `𝕂` has strict Fréchet derivative
`1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero.  -/
hasStrictFDerivAt_exp_zero_of_radius_pos : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [CharZero 𝕂]
  [inst_3 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸],
  0 < (NormedSpace.expSeries 𝕂 𝔸).radius → HasStrictFDerivAt NormedSpace.exp 1 0
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_pf_right : ∀ {R : Type u_1} [inst : CommSemiring R] {a b₃ c : R} (b₁ : R) (b₂ : ℕ), a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c