mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.MappingConeCompHomotopyEquiv.hom f g)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.MappingConeCompHomotopyEquiv.inv f g) h) =
    h
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] {x y : Lex (HahnSeries Γ R)},
  ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔
    (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.preservesLimit_restrictScalars : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_1, u_3} J] (F : CategoryTheory.Functor J (ModuleCat S))
  [Small.{v, max u_3 v} ↑(F.comp (CategoryTheory.forget (ModuleCat S))).sections],
  CategoryTheory.Limits.PreservesLimit F (ModuleCat.restrictScalars f)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Evaluation at a fixed point is uniformly continuous on `α →ᵤ β`.  -/
UniformFun.uniformContinuous_eval : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (x : α), UniformContinuous (Function.eval x ∘ ⇑UniformFun.toFun)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isLocallyFiniteMeasureSMulNNReal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsLocallyFiniteMeasure μ] (c : NNReal), MeasureTheory.IsLocallyFiniteMeasure (c • μ)
-- Mathlib.Order.SupClosed
latticeClosure_min : ∀ {α : Type u_3} [inst : Lattice α] {s t : Set α}, s ⊆ t → IsSublattice t → latticeClosure s ⊆ t
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) (CochainComplex.mappingCone.desc φ α β eq) = β
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_add : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {f : Π₀ (i : ι), β i}
  {h₁ h₂ : (i : ι) → β i → γ}, (f.sum fun i b => h₁ i b + h₂ i b) = f.sum h₁ + f.sum h₂
-- Lean.Elab.Do.Basic
Lean.Elab.Do.mkDoElemElabAttribute : Lean.Name → IO (Lean.KeyedDeclsAttribute Lean.Elab.Do.DoElab)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = true ↔ ∀ (a : α), m.contains a = false
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {γ : Type u_4}
  [inst_1 : TopologicalSpace γ] {g : γ → α}, Semicontinuous r → Continuous g → Semicontinuous (r ∘ g)
-- Mathlib.Analysis.Complex.ReImTopology
Complex.interior_preimage_im : ∀ (s : Set ℝ), interior (Complex.im ⁻¹' s) = Complex.im ⁻¹' interior s
-- Mathlib.Data.EReal.Operations
EReal.addLECancellable_coe : ∀ (x : ℝ), AddLECancellable ↑x
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.Config.mk.injEq : ∀ (toConfig : Mathlib.Tactic.AtomM.Recurse.Config) (ifUnchanged : Mathlib.Tactic.BehaviorIfUnchanged)
  (mode : Mathlib.Tactic.RingNF.RingMode) (toConfig_1 : Mathlib.Tactic.AtomM.Recurse.Config)
  (ifUnchanged_1 : Mathlib.Tactic.BehaviorIfUnchanged) (mode_1 : Mathlib.Tactic.RingNF.RingMode),
  ({ toConfig := toConfig, ifUnchanged := ifUnchanged, mode := mode } =
      { toConfig := toConfig_1, ifUnchanged := ifUnchanged_1, mode := mode_1 }) =
    (toConfig = toConfig_1 ∧ ifUnchanged = ifUnchanged_1 ∧ mode = mode_1)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.mk''_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : D} [inst_5 : CategoryTheory.ModObj A M]
  [inst_6 : CategoryTheory.ModObj A N] (f : M ⟶ N)
  (smul_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
          CategoryTheory.ModObj.smul)
      CategoryTheory.Mod.Hom.mk''._auto_1),
  (CategoryTheory.Mod.Hom.mk'' f smul_hom).hom = f
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_sub_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ⌈a - 1⌉ = ⌈a⌉ - 1
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instSubsingletonOfIsEmpty : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [IsEmpty α], Subsingleton (MeasureTheory.VectorMeasure α M)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {p : Filter ι} [inst_2 : UniformSpace γ] {G : ι → α → γ} {g : α → γ},
  TendstoLocallyUniformly F f p →
    TendstoLocallyUniformly G g p → TendstoLocallyUniformly (fun n x => (F n x, G n x)) (fun x => (f x, g x)) p
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_surjective : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K], Function.Surjective ⇑(Algebra.normalizedTrace F K)
-- Mathlib.Order.Antichain
IsAntichain.antisymm : ∀ {α : Type u_1} {r : α → α → Prop}, IsAntichain r Set.univ → Std.Antisymm r
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The inf of two `NonUnitalSubring`s is their intersection.  -/
NonUnitalSubring.instMin : {R : Type u} → [inst : NonUnitalNonAssocRing R] → Min (NonUnitalSubring R)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.eq_one_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M],
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id M))
      CategoryTheory.MonObj.mul
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.ofSimplex_objEquiv_symm_id : ∀ (n : ℕ), SSet.Subcomplex.ofSimplex (SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id { len := n })) = ⊤
-- Mathlib.Data.Finsupp.Defs
/-- `Finsupp.onFinset s f hf` is the finsupp function representing `f` restricted to the finset `s`.
The function must be `0` outside of `s`. Use this when the set needs to be filtered anyways,
otherwise a better set representation is often available.  -/
Finsupp.onFinset : {α : Type u_1} → {M : Type u_4} → [inst : Zero M] → (s : Finset α) → (f : α → M) → (∀ (a : α), f a ≠ 0 → a ∈ s) → α →₀ M
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.head?_dropWhile_not.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : α) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instAlgebra : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module A V] → (ρ : Representation A G V) → Algebra A (ρ.IntertwiningMap ρ)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instDecidableEq.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : DecidableEq R] [inst_2 : DecidableEq M],
  AddMonoidAlgebra.instDecidableEq = AddMonoidAlgebra.coeffEquiv.decidableEq
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- Any (locally-closed) immersion can be factored into
a closed immersion followed by a (dominant) open immersion.
 -/
AlgebraicGeometry.Scheme.Hom.liftCoborder_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.liftCoborder f)
      (AlgebraicGeometry.Scheme.Hom.coborderRange f).ι =
    f
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- A lower block-triangular matrix is invertible iff both elements of its diagonal are.

This is a propositional form of `Matrix.fromBlocksZero₁₂InvertibleEquiv` forms an `iff`.  -/
Matrix.isUnit_fromBlocks_zero₁₂ : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α},
  IsUnit (Matrix.fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.support_map_subset : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R),
  (Polynomial.map f p).support ⊆ p.support
-- Mathlib.Topology.Algebra.ConstMulAction
Dense.vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (c : G) {s : Set α}, Dense s → Dense (c +ᵥ s)
-- Lean.Parser.Term.Basic
Lean.Parser.tacticParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdealHom_apply : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : Ideal R), (FractionalIdeal.coeIdealHom S P) I = ↑I
-- Mathlib.Topology.Sequences
/-- The disjoint union of an indexed family of sequential spaces is a sequential space.  -/
Sigma.instSequentialSpace : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SequentialSpace (X i)],
  SequentialSpace ((i : ι) × X i)
-- Aesop.Tree.ExtractScript
Aesop.GoalRef.extractScriptCore : Aesop.GoalRef → Aesop.ExtractScriptM Unit
-- Mathlib.RingTheory.Ideal.Operations
Submodule.algebraIdeal : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_3} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Algebra (Ideal R) (Submodule R A)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.const.eq_1 : Nat.Partrec.Code.const 0 = Nat.Partrec.Code.zero
-- Mathlib.Data.Set.Insert
Set.subset_singleton_iff_eq : ∀ {α : Type u_1} {s : Set α} {x : α}, s ⊆ {x} ↔ s = ∅ ∨ s = {x}
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_orElse.match_1.eq_2 : ∀ {σ ε α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : ε) (s' : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (a : ε) → (s' : σ) → motive (EStateM.Result.error a s')),
  (match EStateM.Result.error a s' with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error a s' => h_2 a s') =
    h_2 a s'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ordCompare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtDTreeMap α (fun x => β) compare}
  [inst_2 : Inhabited α] {k : α} {f : β → β},
  compare (Std.ExtDTreeMap.Const.modify t k f).maxKey! t.maxKey! = Ordering.eq
-- Init.Data.Nat.Lcm
Nat.lcm_zero_right : ∀ (m : ℕ), m.lcm 0 = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- **Alias** of `ContMDiffAt.curry_left`.

---

Curried `C^n` functions are `C^n` in the first coordinate.  -/
ContMDiffAt.along_fst : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {y : M'},
  ContMDiffAt (I.prod I') J n (Function.uncurry f) (x, y) → ContMDiffAt I J n (fun x => f x y) x
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- In `ℝ` or `ℂ` fields, the inner product on tensor products is essentially just the inner product
with multiplication instead of tensors, i.e., `⟪a ⊗ₜ b, c ⊗ₜ d⟫ = ⟪a * b, c * d⟫`.  -/
RCLike.inner_tmul_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (a b c d : 𝕜), inner 𝕜 (a ⊗ₜ[𝕜] b) (c ⊗ₜ[𝕜] d) = inner 𝕜 (a * b) (c * d)
-- Mathlib.RingTheory.Localization.FractionRing
/-- If `A` is a commutative ring with fraction field `K`, then the subfield of `K` generated by
the image of `algebraMap A K` is equal to the whole field `K`.  -/
IsFractionRing.closure_range_algebraMap : ∀ (A : Type u_4) [inst : CommRing A] (K : Type u_5) [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K],
  Subfield.closure (Set.range ⇑(algebraMap A K)) = ⊤
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- A cone `t` of `K : J ⥤ Over X` is a limit if and only if the corresponding cone
`coneLift t` of `liftFromOver.obj K : WithTerminal K ⥤ C` is a limit.  -/
CategoryTheory.WithTerminal.isLimitEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Over X)} →
            {t : CategoryTheory.Limits.Cone K} →
              CategoryTheory.Limits.IsLimit (CategoryTheory.WithTerminal.coneEquiv.functor.obj t) ≃
                CategoryTheory.Limits.IsLimit t
-- Mathlib.Geometry.RingedSpace.Stalks
/-- If `α = β` and `x = x'`, we would like to say that `stalk_map α x = stalk_map β x'`.
Unfortunately, this equality is not well-formed, as their types are not _definitionally_ the same.
To get a proper congruence lemma, we therefore have to introduce these `eqToHom` arrows on
either side of the equality.
 -/
AlgebraicGeometry.PresheafedSpace.stalkMap.congr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α β : X ⟶ Y) (h₁ : α = β) (x x' : ↑↑X) (h₂ : x = x'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap β x')
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mk_of_neg_add : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (x : G ⊕ H),
  AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.map Neg.neg Neg.neg x)) + AddMonoid.Coprod.mk (FreeAddMonoid.of x) = 0
-- Mathlib.Topology.Maps.Basic
IsOpenMap.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ {x : X}, ContinuousAt f x → Filter.map f (nhds x) = nhds (f x)
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_one_near_10 : |Real.exp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10
-- Init.Data.Range.Polymorphic.Char
_private.Init.Data.Range.Polymorphic.Char.0.Char.instPreservesRxoSizeFinNumCodePointsMap : Char.map✝.PreservesRxoSize
-- Mathlib.Algebra.Homology.ImageToKernel
/-- Prefer `imageToKernel`.  -/
subobject_ofLE_as_imageToKernel : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0)
  (h : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g),
  (CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) h = imageToKernel f g w
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_I₀ : ∀ {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤),
  (AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop s hs).I₀ = ι
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.image_op_vadd_distrib : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : Add β] [inst_2 : FunLike F α β]
  [AddHomClass F α β] (f : F) (a : α) (s : Set α), ⇑f '' (AddOpposite.op a +ᵥ s) = AddOpposite.op (f a) +ᵥ ⇑f '' s
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.add_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  {M N : CategoryTheory.Mat_ C} (f g : M ⟶ N) (i : M.ι) (j : N.ι), (f + g) i j = f i j + g i j
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.precompose_pt : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes)
  {G : CategoryTheory.Functor J (Type w₀')} (app : (j : J) → G.obj j → F.obj j)
  (naturality :
    ∀ {j j' : J} (f : j ⟶ j'),
      app j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map f)) =
        ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ∘ app j),
  (c.precompose app naturality).pt = c.pt
-- Mathlib.Analysis.InnerProductSpace.Spectrum
inner_product_apply_eigenvector : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E}, T v = μ • v → inner 𝕜 v (T v) = μ * ↑‖v‖ ^ 2
-- Std.Time.Format.DateFormat
Std.Time.DateFormat.mk.injEq : ∀ (firstDayOfWeek : Std.Time.Weekday) (minimalDaysInFirstWeek : Std.Time.Internal.Bounded.LE 0 6)
  (symbols : Std.Time.DateFormatSymbols) (firstDayOfWeek_1 : Std.Time.Weekday)
  (minimalDaysInFirstWeek_1 : Std.Time.Internal.Bounded.LE 0 6) (symbols_1 : Std.Time.DateFormatSymbols),
  ({ firstDayOfWeek := firstDayOfWeek, minimalDaysInFirstWeek := minimalDaysInFirstWeek, symbols := symbols } =
      { firstDayOfWeek := firstDayOfWeek_1, minimalDaysInFirstWeek := minimalDaysInFirstWeek_1,
        symbols := symbols_1 }) =
    (firstDayOfWeek = firstDayOfWeek_1 ∧ minimalDaysInFirstWeek = minimalDaysInFirstWeek_1 ∧ symbols = symbols_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.lift_map_homMk : ∀ {V : SSet.Truncated 2} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  (obj : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }) → D)
  (map :
    {x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })} →
      SSet.Truncated.Edge x y → (obj x ⟶ obj y))
  (map_id :
    ∀ (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
      map (SSet.Truncated.Edge.id x) = CategoryTheory.CategoryStruct.id (obj x))
  (map_comp :
    ∀ {x₀ x₁ x₂ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
      {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
      (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂)
  {x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  (e : SSet.Truncated.Edge x y),
  (SSet.Truncated.HomotopyCategory.lift obj (fun {x y} => map) map_id ⋯).map (SSet.Truncated.HomotopyCategory.homMk e) =
    map e
-- Mathlib.Data.Rat.Cast.Defs
/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the positive naturals and `-1` then
they are equal.  -/
MonoidWithZeroHomClass.ext_rat_on_pnat : ∀ {F : Type u_1} {M₀ : Type u_5} [inst : MonoidWithZero M₀] [inst_1 : FunLike F ℚ M₀] [MonoidWithZeroHomClass F ℚ M₀]
  {f g : F}, f (-1) = g (-1) → (∀ (n : ℕ), 0 < n → f ↑n = g ↑n) → f = g
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Sym2.map_mk`. -/
Sym2.map_pair_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a b : α), Sym2.map f s(a, b) = s(f a, f b)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instFromJsonRequestID : Lean.FromJson Lean.JsonRpc.RequestID
-- Mathlib.RingTheory.Ideal.Quotient.Basic
/-- `R^n/I^n` is isomorphic to `(R/I)^n` as an `R/I`-module.  -/
Ideal.piQuotEquiv : (ι : Type u_1) →
  {R : Type u_3} →
    [inst : Ring R] → (I : Ideal R) → [inst_1 : I.IsTwoSided] → ((ι → R) ⧸ Ideal.pi fun x => I) ≃ₗ[R ⧸ I] ι → R ⧸ I
-- Mathlib.Topology.Maps.Basic
/-- Assume `f` is a closed map. If some property `p` holds around every point in the fiber of `f`
at `y₀`, then for any `y` close enough to `y₀` we have that `p` holds on the fiber at `y`.  -/
IsClosedMap.eventually_nhds_fiber : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f →
    ∀ {p : X → Prop} (y₀ : Y),
      (∀ x₀ ∈ f ⁻¹' {y₀}, ∀ᶠ (x : X) in nhds x₀, p x) → ∀ᶠ (y : Y) in nhds y₀, ∀ x ∈ f ⁻¹' {y}, p x
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.ofPowerSeries_X : ∀ {Γ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : Semiring Γ] [inst_2 : PartialOrder Γ]
  [inst_3 : IsStrictOrderedRing Γ], (HahnSeries.ofPowerSeries Γ R) PowerSeries.X = (HahnSeries.single 1) 1
-- Mathlib.LinearAlgebra.Reflection
/-- A formula for $(r_1 r_2)^m$, where $m$ is a natural number.  -/
Module.reflection_mul_reflection_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℕ) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_pow._auto_1 →
    ↑((Module.reflection hf * Module.reflection hg) ^ m) =
      LinearMap.id +
          (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)) *
              (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) +
                Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 3) / 2)))) •
            (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
        (Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (Polynomial.Chebyshev.S R (↑m / 2)) +
              Polynomial.eval t (Polynomial.Chebyshev.S R ((↑m - 2) / 2)))) •
          (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y)
-- Mathlib.CategoryTheory.Abelian.Subobject
CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C)
  (a : CategoryTheory.Subobject X),
  (CategoryTheory.Abelian.subobjectIsoSubobjectOp X) a =
    CategoryTheory.Subobject.lift (fun x f x_1 => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op) ⋯
      a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- Construct a walk from a list of vertices where adjacent vertices in the list are also adjacent
in the graph  -/
SimpleGraph.Walk.ofSupport : {V : Type u} →
  {G : SimpleGraph V} → (l : List V) → (hne : l ≠ []) → List.IsChain G.Adj l → G.Walk (l.head hne) (l.getLast hne)