mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Ext
CommRing.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : CommRing R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_cof : ∀ {o : Ordinal.{u_1}}, Order.IsSuccLimit o → o.cof.IsRegular
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.toList.match_1.eq_1 : ∀ {α : Type u_1} (motive : Lists α → Sort u_2) (fst : Bool) (l : Lists' α fst)
  (h_1 : (fst : Bool) → (l : Lists' α fst) → motive ⟨fst, l⟩),
  (match ⟨fst, l⟩ with
    | ⟨fst, l⟩ => h_1 fst l) =
    h_1 fst l
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens) (x : ↥U) (hx : x ∈ V),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) ↑x ⋯)
      (U.stalkIso x).inv =
    (↑U).presheaf.germ V x hx
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.bitraverse_eq_bimap_id : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {α α' β β' : Type u}
  (f : α → β) (f' : α' → β') (x : t α α'), bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.u_l_top : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop α] {l : α → β} {u : β → α},
  GaloisConnection l u → u (l ⊤) = ⊤
-- Mathlib.Topology.ContinuousMap.Lattice
ContinuousMap.instIsOrderedMonoid : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : TopologicalSpace β] [inst_2 : PartialOrder β]
  [inst_3 : CommMonoid β] [IsOrderedMonoid β] [inst_5 : ContinuousMul β], IsOrderedMonoid C(α, β)
-- Mathlib.Algebra.Order.Group.PosPart
posPart_negPart_injective : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α], Function.Injective fun a => (a⁺, a⁻)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.dvd_coord_smul : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι) (m : M) (r : R), r ∣ (b.coord i) (r • m)
-- Mathlib.Probability.Moments.SubGaussian
/-- A random variable `X` has a conditionally sub-Gaussian moment-generating function
with parameter `c` with respect to a sigma-algebra `m` and a measure `μ` if for all `t : ℝ`,
`exp (t * X)` is `μ`-integrable and the moment-generating function of `X` conditioned on `m` is
almost surely bounded by `exp (c * t ^ 2 / 2)` for all `t : ℝ`.
This implies in particular that `X` has expectation 0.

The actual definition uses `Kernel.HasSubgaussianMGF`: `HasCondSubgaussianMGF` is defined as
sub-Gaussian with respect to the conditional expectation kernel for `m` and the restriction of `μ`
to the sigma-algebra `m`.  -/
ProbabilityTheory.HasCondSubgaussianMGF : {Ω : Type u_1} →
  (m : MeasurableSpace Ω) →
    {mΩ : MeasurableSpace Ω} →
      m ≤ mΩ →
        [StandardBorelSpace Ω] →
          (Ω → ℝ) →
            NNReal →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasCondSubgaussianMGF._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Mathlib.Topology.Compactness.SigmaCompact
IsClosed.sigmaCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [SigmaCompactSpace X] {s : Set X}, IsClosed s → SigmaCompactSpace ↑s
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.coe_induceHom : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ : G →g G')
  (φst : Set.MapsTo (⇑φ) s t), ⇑(SimpleGraph.induceHom φ φst) = Set.MapsTo.restrict (⇑φ) s t φst
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `orthogonal` reverses the `≤` ordering of two
subspaces.  -/
ClosedSubmodule.orthogonal_le : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₁ K₂ : ClosedSubmodule 𝕜 E}, K₁ ≤ K₂ → K₂ᗮ ≤ K₁ᗮ
-- Init.Data.UInt.BasicAux
/-- Converts 16-bit unsigned integers to 32-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.toUInt32 : UInt16 → UInt32
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsRight.iInf : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u_1}
  {W : ι → CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C}
  [∀ (i : ι), (W i).RespectsRight Q], (⨅ i, W i).RespectsRight Q
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Extract the finite pattern given by restricting a configuration `x : G → A`
to a finite subset `U : Finset G`.

The pattern has `config g = x g` for `g ∈ U` and `config g = default` outside `U`,
with support `U`. In other words, `Pattern.fromConfig x U` is the partial configuration of
`x` visible on the coordinates in `U`, padded with `default` elsewhere.  -/
SymbolicDynamics.FullShift.Pattern.fromConfig : {A : Type u_1} → [inst : Inhabited A] → {G : Type u_2} → (G → A) → Finset G → SymbolicDynamics.FullShift.Pattern A G
-- Mathlib.Topology.UniformSpace.Cauchy
/-- If a Cauchy sequence has a convergent subsequence, then it converges.  -/
tendsto_nhds_of_cauchySeq_of_subseq : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] {u : β → α},
  CauchySeq u →
    ∀ {ι : Type u_1} {f : ι → β} {p : Filter ι} [p.NeBot],
      Filter.Tendsto f p Filter.atTop →
        ∀ {a : α}, Filter.Tendsto (u ∘ f) p (nhds a) → Filter.Tendsto u Filter.atTop (nhds a)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instTop.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M],
  SaturatedAddSubmonoid.instTop =
    {
      top :=
        let __src := ⊤;
        { toAddSubmonoid := __src, addSaturated := ⋯ } }
-- Mathlib.NumberTheory.Divisors
Int.divisors_eq_empty : ∀ {z : ℤ}, z.divisors = ∅ ↔ z = 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_const : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (c : E) [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.MemLp (fun x => c) p μ
-- Mathlib.Analysis.Convex.StrictConvexBetween
AffineMap.ofMapMidpoint.eq_1 : ∀ {V : Type u_1} {P : Type u_2} {W : Type u_3} {Q : Type u_4} [inst : SeminormedAddCommGroup V]
  [inst_1 : PseudoMetricSpace P] [inst_2 : NormedAddTorsor V P] [inst_3 : NormedAddCommGroup W] [inst_4 : MetricSpace Q]
  [inst_5 : NormedAddTorsor W Q] [inst_6 : NormedSpace ℝ V] [inst_7 : NormedSpace ℝ W] (f : P → Q)
  (h : ∀ (x y : P), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)) (hfc : Continuous f),
  AffineMap.ofMapMidpoint f h hfc =
    AffineMap.mk' f
      (↑((AddMonoidHom.ofMapMidpoint ℝ ℝ
              (⇑(AffineEquiv.vaddConst ℝ (f (Classical.arbitrary P))).symm ∘
                f ∘ ⇑(AffineEquiv.vaddConst ℝ (Classical.arbitrary P)))
              ⋯ ⋯).toRealLinearMap
          ⋯))
      (Classical.arbitrary P) ⋯
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapPresentation_relation : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin n),
  (MvPolynomial.universalFactorizationMapPresentation R n m k hn).relation i =
    MvPolynomial.C (MvPolynomial.X i) -
      (MvPolynomial.map MvPolynomial.C)
        ((MvPolynomial.tensorEquivSum R (Fin m) (Fin k) R)
          ((MvPolynomial.universalFactorizationMap R n m k hn) (MvPolynomial.X i)))
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- The degree-`n` power sum symmetric `MvPolynomial σ R`.
It is the sum over all the `n`-th powers of the variables.  -/
MvPolynomial.psum : (σ : Type u_5) → (R : Type u_6) → [inst : CommSemiring R] → [Fintype σ] → ℕ → MvPolynomial σ R
-- Mathlib.RingTheory.Filtration
/-- The `sInf` of a family of `I.Filtration`s is an `I.Filtration`.  -/
Ideal.Filtration.instInfSet : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → InfSet (I.Filtration M)
-- Mathlib.Topology.Order.ExtendFrom
eq_lim_at_left_extendFrom_uIoo : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [DenselyOrdered α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β} {a b : α} {la : β} [T2Space β],
  a ≠ b → Filter.Tendsto f (nhdsWithin a (Set.uIoo a b)) (nhds la) → extendFrom (Set.uIoo a b) f a = la
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT?.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a)),
  Std.DTreeMap.Internal.Impl.getEntryLT?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- `L` spans the full space `E` over `K`.  -/
IsZLattice.span_top : ∀ {K : Type u_1} {inst : NormedField K} {E : Type u_2} {inst_1 : NormedAddCommGroup E} {inst_2 : NormedSpace K E}
  {L : Submodule ℤ E} {inst_3 : DiscreteTopology ↥L} [self : IsZLattice K L], Submodule.span K ↑L = ⊤
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
/-- Construct limit data for a binary product in `ModuleCat R`, using `ModuleCat.of R (M × N)`.
 -/
ModuleCat.binaryProductLimitCone : {R : Type u} → [inst : Ring R] → (M N : ModuleCat R) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair M N)
-- Mathlib.ModelTheory.Definability
Set.Definable.eq_1 : ∀ {M : Type w} (A : Set M) (L : FirstOrder.Language) [inst : L.Structure M] {α : Type u₁} (s : Set (α → M)),
  A.Definable L s = ∃ φ, s = Set.ofPred φ.Realize
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is an `AddZeroClass` under pointwise operations if `α` is.  -/
Set.addZeroClass : {α : Type u_2} → [AddZeroClass α] → AddZeroClass (Set α)
-- Mathlib.Tactic.Linarith.Frontend
/-- Given a list `ls` of pairs `(α, L)` where each `L` is a list of indexed proofs of
comparisons over the type `α`, `findLinarithContradiction cfg g ls` tries each list in
succession, invoking `linarith` until one produces a contradiction. It returns the
resulting proof of `False` together with the indices of the hypotheses that had
nonzero coefficients in the final certificate.
 -/
Mathlib.Tactic.Linarith.findLinarithContradiction : Mathlib.Tactic.Linarith.LinarithConfig →
  Lean.MVarId → List (Lean.Expr × List (Lean.Expr × ℕ)) → Lean.MetaM (Lean.Expr × List ℕ)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sound : ∀ {x y : PSet.{u_1}}, x.Equiv y → ZFSet.mk x = ZFSet.mk y
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- Mapping a walk to its own subgraph and then to the original graph produces the same walk.  -/
SimpleGraph.Walk.map_mapToSubgraph_hom : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v), SimpleGraph.Walk.map w.toSubgraph.hom w.mapToSubgraph = w
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The (unique) left homology map data associated to a morphism of short complexes that
are both equipped with left homology data.  -/
CategoryTheory.ShortComplex.leftHomologyMapData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h₁ : S₁.LeftHomologyData) →
            (h₂ : S₂.LeftHomologyData) → CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂
-- Lean.Meta.DiscrTree.Basic
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.keysAsPattern.goN : ℕ → StateRefT' IO.RealWorld (List Lean.Meta.DiscrTree.Key) Lean.CoreM (Array Lean.MessageData)
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Translation by `v` (that is, the map `p ↦ v +ᵥ p`) as an affine isometric automorphism of `P`.
 -/
AffineIsometryEquiv.constVAdd : (𝕜 : Type u_1) →
  {V : Type u_2} →
    (P : Type u_10) →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] → [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → V → P ≃ᵃⁱ[𝕜] P
-- Aesop.Tree.Data
Aesop.RappId.toNat : Aesop.RappId → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.compl_isIndContained_compl : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, Gᶜ.IsIndContained Hᶜ ↔ G.IsIndContained H
-- Mathlib.Data.NNReal.Defs
/-- Every real number nonnegative or nonpositive, phrased using `ℝ≥0`.  -/
Real.nnreal_dichotomy : ∀ (r : ℝ), ∃ x, r = ↑x ∨ r = -↑x
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyKey.mk.sizeOf_spec : ∀ (numGoals nameLength replacementSize : ℕ) (name : String) (newGoals : Array Lean.Meta.AbstractMVarsResult),
  sizeOf
      { numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        newGoals := newGoals } =
    1 + sizeOf numGoals + sizeOf nameLength + sizeOf replacementSize + sizeOf name + sizeOf newGoals
-- Mathlib.SetTheory.Lists
Lists'.atom.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : α), sizeOf (Lists'.atom a) = 1 + sizeOf a
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.le_prod_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {s : AddSubsemigroup M} {t : AddSubsemigroup N}
  {u : AddSubsemigroup (M × N)},
  u ≤ s.prod t ↔ AddSubsemigroup.map (AddHom.fst M N) u ≤ s ∧ AddSubsemigroup.map (AddHom.snd M N) u ≤ t
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- Let `u : E →L[𝕜] F` be a Fredholm operator. Given `dom₁` (resp. `codom₀`) an arbitrary
topological complement of `u.ker` (resp. `u.range`), we get a `FredholmPackage` for `u`
by considering the decompositions `E = dom₁ ⊕ u.ker`, `F = u.range ⊕ codom₀`, and the isomorphism
`dom₁ ≃L[𝕜] u.range` induced by `u`.

If you need control over the decompositions, this is the primary way to get a `FredholmPackage`.
Otherwise, see `IsFredholm.nonempty_fredholmPackage`.  -/
ContinuousLinearMap.IsFredholm.fredholmPackage : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] →
                  [inst_6 : TopologicalSpace F] →
                    [IsTopologicalAddGroup E] →
                      {u : E →L[𝕜] F} →
                        u.IsFredholm →
                          {dom₁ : Submodule 𝕜 E} →
                            {codom₀ : Submodule 𝕜 F} →
                              Submodule.IsTopCompl (↑u).ker dom₁ →
                                Submodule.IsTopCompl (↑u).range codom₀ → u.FredholmPackage
-- Init.Sym.Lemmas
Lean.Sym.decide_isTrue_congr : ∀ (p p' : Prop), p = p' → ∀ {inst : Decidable p} {hp : p'}, decide p = true
-- Init.Prelude
instDecidableOr : {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instIsConcreteLEFinset : ∀ {ι : Type u_1}, IsConcreteLE (AbstractSimplicialComplex ι) (Finset ι)
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_iff_left : ∀ {n a b c d : ℕ}, a ≡ b [MOD n] → (a + c ≡ b + d [MOD n] ↔ c ≡ d [MOD n])
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (α : Type t)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Y),
  (CategoryTheory.Limits.FormalCoproduct.powerFunctor α).map f = CategoryTheory.Limits.FormalCoproduct.powerMap f α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The category of binary bicones on a given diagram.  -/
CategoryTheory.Limits.BinaryBicone.category : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → CategoryTheory.Category.{uC', max uC uC'} (CategoryTheory.Limits.BinaryBicone P Q)
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The sum of almost everywhere strongly measurable functions is measurable.  -/
MeasureTheory.AEStronglyMeasurable.tsum : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [ContinuousAdd E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [Countable ι] {μ : MeasureTheory.Measure X} {f : ι → X → E},
  (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
    MeasureTheory.AEStronglyMeasurable (fun x => ∑'[L] (i : ι), f i x) μ
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_adjunction_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {L R : CategoryTheory.Functor C C} (adj : L ⊣ R)
  (α : CategoryTheory.Functor.id C ⟶ L) (c : C),
  ((CategoryTheory.conjugateEquiv adj CategoryTheory.Adjunction.id) α).app c =
    CategoryTheory.CategoryStruct.comp (α.app (R.obj c)) (adj.counit.app c)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The definition of `Cospherical`.  -/
EuclideanGeometry.cospherical_def : ∀ {P : Type u_2} [inst : MetricSpace P] (ps : Set P),
  EuclideanGeometry.Cospherical ps ↔ ∃ center radius, ∀ p ∈ ps, dist p center = radius
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqPower.beq.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Power → Sort u_1) (a : Lean.Grind.CommRing.Var) (a_1 : ℕ)
  (b : Lean.Grind.CommRing.Var) (b_1 : ℕ)
  (h_1 :
    (a : Lean.Grind.CommRing.Var) →
      (a_2 : ℕ) → (b : Lean.Grind.CommRing.Var) → (b_2 : ℕ) → motive { x := a, k := a_2 } { x := b, k := b_2 })
  (h_2 : (x x_1 : Lean.Grind.CommRing.Power) → motive x x_1),
  (match { x := a, k := a_1 }, { x := b, k := b_1 } with
    | { x := a, k := a_2 }, { x := b, k := b_2 } => h_1 a a_2 b b_2
    | x, x_1 => h_2 x x_1) =
    h_1 a a_1 b b_1
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_le_card : ∀ {o₁ o₂ : Ordinal.{u_1}}, o₁ ≤ o₂ → o₁.card ≤ o₂.card
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl : (Type u → Type u) → Type u → Type u
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.isIso_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.left
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.algebraRight : {𝕜 : Type u_2} →
  {𝕝 : Type u_3} →
    {α : Type u_5} →
      [inst : PartialOrder α] →
        [inst_1 : LocallyFiniteOrder α] →
          [inst_2 : DecidableEq α] →
            [inst_3 : CommSemiring 𝕜] → [inst_4 : CommSemiring 𝕝] → [Algebra 𝕜 𝕝] → Algebra 𝕜 (IncidenceAlgebra 𝕝 α)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.HasBasis.uniformity_of_nhds_one_inv_mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Sort u_3} {p : ι → Prop}
  {U : ι → Set α}, (nhds 1).HasBasis p U → (uniformity α).HasBasis p fun i => {x | x.1⁻¹ * x.2 ∈ U i}
-- Lean.ResolveName
/-- Check exact name  -/
_private.Lean.ResolveName.0.Lean.ResolveName.resolveExact : Lean.Environment → Lean.Options → Lean.Name → Option Lean.Name
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.comap_cond : ∀ {Ω : Type u_1} {Ω' : Type u_2} {m : MeasurableSpace Ω} {m' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω}
  {s : Set Ω} {i : Ω' → Ω},
  MeasurableEmbedding i →
    (∀ᵐ (ω : Ω) ∂μ, ω ∈ Set.range i) →
      MeasurableSet s → MeasureTheory.Measure.comap i μ[|s] = (MeasureTheory.Measure.comap i μ)[|i ⁻¹' s]
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_Ioo : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a b : R},
  0 ≤ a → Nat.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋₊ ⌈b⌉₊
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piConst_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X Y : C}
  (f : X ⟶ Y) (n : Type wᵒᵖ), (CategoryTheory.Limits.piConst.map f).app n = CategoryTheory.Limits.Pi.map fun x => f
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.MkSimpContextResult.mk.inj : ∀ {ctx : Lean.Meta.Simp.Context} {simprocs : Lean.Meta.Simp.SimprocsArray}
  {dischargeWrapper : Lean.Elab.Tactic.Simp.DischargeWrapper}
  {simpArgs : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)} {ctx_1 : Lean.Meta.Simp.Context}
  {simprocs_1 : Lean.Meta.Simp.SimprocsArray} {dischargeWrapper_1 : Lean.Elab.Tactic.Simp.DischargeWrapper}
  {simpArgs_1 : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)},
  { ctx := ctx, simprocs := simprocs, dischargeWrapper := dischargeWrapper, simpArgs := simpArgs } =
      { ctx := ctx_1, simprocs := simprocs_1, dischargeWrapper := dischargeWrapper_1, simpArgs := simpArgs_1 } →
    ctx = ctx_1 ∧ simprocs = simprocs_1 ∧ dischargeWrapper = dischargeWrapper_1 ∧ simpArgs = simpArgs_1
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.parseFirstByte_eq_twoMore_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {i : ℕ} {c : Char},
  b.utf8DecodeChar? i = some c →
    c.utf8Size = 3 →
      ∀ (h' : i < b.size), ByteArray.utf8DecodeChar?.parseFirstByte b[i] = ByteArray.utf8DecodeChar?.FirstByte.twoMore
-- Mathlib.Data.ENat.Basic
ENat.succ_def : ∀ (m : ℕ∞), Order.succ m = m + 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a k : α} {v : β k}, (t.insert k v).getKey? a = if cmp k a = Ordering.eq then some k else t.getKey? a
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.eval₂Hom_comp_C : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (g : σ → S), (MvPolynomial.eval₂Hom f g).comp MvPolynomial.C = f
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.final_functor : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  (∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)) → (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functor J κ).Final
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage S hkf hcc fac).hom
      (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) =
    CategoryTheory.CategoryStruct.comp ι (S.isoOpcyclesOfIsColimit hcc).hom
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_succ : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}),
  Ordinal.deriv f (Order.succ o) = Ordinal.nfp f (Order.succ (Ordinal.deriv f o))