mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, t.size ≤ (Std.DTreeMap.Internal.Impl.erase! k t).size + 1
-- Batteries.Control.AlternativeMonad
/-- Mapping the result of a failure is still a failure  -/
LawfulAlternative.map_failure : ∀ {m : Type u_1 → Type u_2} {inst : Alternative m} [self : LawfulAlternative m] {α β : Type u_1} (f : α → β),
  f <$> failure = failure
-- Lean.Message
Lean.MessageData.ofGoal : Lean.MVarId → Lean.MessageData
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications `M` and `M₂` will be topological modules over the topological
ring `R`.  -/
«term_→L[_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Finsupp.Indicator
Finsupp.indicator_of_mem : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] {s : Finset ι} {i : ι} (hi : i ∈ s) (f : (i : ι) → i ∈ s → α),
  (Finsupp.indicator s f) i = f i hi
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instDecidableLtOfDay : {x y : Std.Time.Nanosecond.Ordinal.OfDay} → Decidable (x < y)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgEquiv.subsingleton_right : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [Subsingleton (Subalgebra R B)], Subsingleton (A ≃ₐ[R] B)
-- Mathlib.Order.Compare
cmp_eq_eq_iff : ∀ {α : Type u_1} [inst : LinearOrder α] (x y : α), cmp x y = Ordering.eq ↔ x = y
-- Mathlib.Data.Vector3
Fin2.insertPerm.eq_3 : ∀ (a : ℕ) (a_1 : Fin2 a.succ), a_1.fs.insertPerm Fin2.fz = Fin2.fz.fs
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C), S.Exact ↔ CategoryTheory.Epi (imageToKernel' S.f S.g ⋯)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.minKey! = k ↔
      (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
/-- The alternating group is the closure of the set of permutations with cycle type (2, 2).  -/
Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  5 ≤ Nat.card α → Subgroup.closure {g | g.cycleType = {2, 2}} = alternatingGroup α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_eq_get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {h : a ∈ t}, Std.ExtDTreeMap.Const.get t a h = (Std.ExtDTreeMap.Const.get? t a).get ⋯
-- Mathlib.Algebra.Ring.Equiv
RingEquivClass.toNonUnitalRingHomClass : ∀ {F : Type u_1} {R : Type u_4} {S : Type u_5} [inst : EquivLike F R S] [inst_1 : NonUnitalNonAssocSemiring R]
  [inst_2 : NonUnitalNonAssocSemiring S] [h : RingEquivClass F R S], NonUnitalRingHomClass F R S
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- If `𝒜` is a measure-dense family of sets and `c : E`, then the set of constant indicators
with constant `c` whose underlying set is in `𝒜` is dense in the set of constant indicators
which are in `Lp E p μ` when `1 ≤ p < ∞`.  -/
MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure : ∀ {X : Type u_1} {E : Type u_2} [m : MeasurableSpace X] [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure X}
  (p : ENNReal) [one_le_p : Fact (1 ≤ p)] [p_ne_top : Fact (p ≠ ⊤)] {𝒜 : Set (Set X)} (h𝒜 : μ.MeasureDense 𝒜) (c : E),
  {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), MeasureTheory.indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), MeasureTheory.indicatorConstLp p ⋯ hμs c = x}
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.surjective_coe : ∀ {α : Type u} [inst : TopologicalSpace α], Function.Surjective ConnectedComponents.mk
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.tendsto_cofinite_zero_of_summable : ∀ {α : Type u_3} {f : α → NNReal}, Summable f → Filter.Tendsto f Filter.cofinite (nhds 0)
-- Mathlib.CategoryTheory.Endomorphism
/-- Units in the monoid of endomorphisms of an object
are (multiplicatively) equivalent to automorphisms of that object.
 -/
CategoryTheory.Aut.unitsEndEquivAut : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X : C) → (CategoryTheory.End X)ˣ ≃* CategoryTheory.Aut X
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toCompleteSpace : ∀ {A : Type u_1} [self : NonUnitalCommCStarAlgebra A], CompleteSpace A
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.Icc_min_max : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Icc (min a b) (max a b) = Set.uIcc a b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {kmi : α}, (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.isCovering_of_bijective_costar : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V)
  [inst_2 : Quiver.HasInvolutiveReverse U] [inst_3 : Quiver.HasInvolutiveReverse V] [φ.MapReverse],
  (∀ (u : U), Function.Bijective (φ.costar u)) → φ.IsCovering
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.iff_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasPullbacks D] {F₁ F₂ F₃ F₄ : CategoryTheory.Functor C D} {f₁ : F₁ ⟶ F₂} {f₂ : F₁ ⟶ F₃}
  {f₃ : F₂ ⟶ F₄} {f₄ : F₃ ⟶ F₄},
  CategoryTheory.IsPullback f₁ f₂ f₃ f₄ ↔
    ∀ (X : C), CategoryTheory.IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.toIsometry_apply : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (g : B₁.IsometryEquiv B₂) (x : M₁), g.toIsometry x = g x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcUnits_pow : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p]
  [inst_10 : ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℕ)
  (hf : autoParam (ContinuousOn f (spectrum R a)) cfcUnits_pow._auto_1) (ha : autoParam (p a) cfcUnits_pow._auto_3),
  cfcUnits f a hf' hf ha ^ n = cfcUnits (fun i => f i ^ n) a ⋯ ⋯ ha
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.measurableAtom_of_countable : ∀ {β : Type u_2} [inst : MeasurableSpace β] [Countable β] (x : β), MeasurableSet (measurableAtom x)
-- Mathlib.Order.Filter.IsBounded
BddAbove.isBoundedUnder : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α} {s : Set β},
  s ∈ f → BddAbove (u '' s) → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Batteries.Data.DList.Lemmas
_private.Batteries.Data.DList.Lemmas.0.Batteries.DList.cons.match_1.eq_1 : ∀ {α : Type u_1} (motive : α → Batteries.DList α → Sort u_2) (a : α) (f : List α → List α)
  (h : ∀ (l : List α), f l = f [] ++ l)
  (h_1 :
    (a : α) → (f : List α → List α) → (h : ∀ (l : List α), f l = f [] ++ l) → motive a { apply := f, invariant := h }),
  (match a, { apply := f, invariant := h } with
    | a, { apply := f, invariant := h } => h_1 a f h) =
    h_1 a f h
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
MDifferentiableAt.continuousAt : ∀ {𝕜 : 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 : M → M'} {x : M},
  MDiffAt f x → ContinuousAt f x
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivAt.const_rpow : ∀ {f : ℝ → ℝ} {f' x a : ℝ}, 0 < a → HasDerivAt f f' x → HasDerivAt (fun x => a ^ f x) (Real.log a * f' * a ^ f x) x
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_fun_finsetProd : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : CommMonoid γ] [inst_3 : ContinuousMul γ] {ι : Type u_5} (s : Finset ι) (f : ι → α →ₘ[μ] γ),
  ↑(∏ i ∈ s, f i) =ᵐ[μ] fun x => ∏ i ∈ s, ↑(f i) x
-- Mathlib.Combinatorics.Quiver.Path
/-- Equality is decidable on all uniformly bounded paths given decidable
equality on the vertices and the arrows.  -/
Quiver.Path.decidableEqBoundedPaths : {V : Type u_1} →
  [inst : Quiver V] →
    [DecidableEq V] →
      [(v w : V) → DecidableEq (v ⟶ w)] → (n : ℕ) → (v w : V) → DecidableEq (Quiver.Path.BoundedPaths v w n)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyQuasiFinite : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.LocallyQuasiFinite
-- Mathlib.Tactic.TacticAnalysis
_private.Mathlib.Tactic.TacticAnalysis.0.Mathlib.TacticAnalysis.Entry.import.unsafe_1 : Mathlib.TacticAnalysis.Entry → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.TacticAnalysis.Config
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a countable family of extended metric spaces,
one may put an extended distance on their product `Π i, E i`.

It is highly non-canonical, though, and therefore not registered as a global instance.
The distance we use here is `edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i))`.  -/
PiCountable.emetricSpace : {ι : Type u_2} → [Encodable ι] → {F : ι → Type u_3} → [(i : ι) → EMetricSpace (F i)] → EMetricSpace ((i : ι) → F i)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.trailingCoeff * q.trailingCoeff ≠ 0 → (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
-- Mathlib.CategoryTheory.Category.Preorder
/-- The categorical equivalence between the category of monotone functions `X →o Y` and the category
of functors `X ⥤ Y`, where `X` and `Y` are preorder categories.  -/
OrderHom.equivalenceFunctor : {X : Type u} → {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → X →o Y ≌ CategoryTheory.Functor X Y
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.dirac_apply : ∀ {α : Type u_1} (a : α) (s : Set α), (MeasureTheory.OuterMeasure.dirac a) s = s.indicator (fun x => 1) a
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex✝ f n).X₃ =
    (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.S✝ f n).homology n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R) (u v : R),
  W'.addY (u • P) (v • Q) = (u * v) ^ 2 * W'.addY P Q
-- Mathlib.Data.Set.Basic
Set.union_congr_right : ∀ {α : Type u} {s t u : Set α}, s ⊆ t ∪ u → t ⊆ s ∪ u → s ∪ u = t ∪ u
-- Mathlib.Topology.Inseparable
Inseparable.map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
  Inseparable x y → Continuous f → Inseparable (f x) (f y)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance is controlled by the diameter of the union.  -/
Metric.hausdorffDist_le_diam : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
  s.Nonempty →
    Bornology.IsBounded s → t.Nonempty → Bornology.IsBounded t → Metric.hausdorffDist s t ≤ Metric.diam (s ∪ t)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHom_mapDomainOfBialgHom : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H),
  MonoidAlgebra.mapDomainBialgHom R (MonoidAlgebra.mapDomainOfBialgHom f) = f
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.id_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (Y : Cᵒᵖ),
  (CategoryTheory.Profunctor.id.obj X).obj Y = (Opposite.unop Y ⟶ X)
-- Std.Sync.Channel
/-- Receive a value from the channel, returning a task that will resolve once the transmission could be
completed. Note that the task may resolve to `none` if the channel was closed before it could be
completed.
 -/
Std.Channel.recv : {α : Type} → [Inhabited α] → Std.Channel α → BaseIO (Task α)
-- Mathlib.Order.Category.BddDistLat
BddDistLat.ofHom_id : ∀ {X : Type u} [inst : DistribLattice X] [inst_1 : BoundedOrder X],
  BddDistLat.ofHom (BoundedLatticeHom.id X) = CategoryTheory.CategoryStruct.id (BddDistLat.of X)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : BEq α]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ [Std.TransCmp cmp] {k : α}, t.keys.contains k = t.contains k
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
multipliableUniformly_iff_hasProdUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  MultipliableUniformly f ↔ HasProdUniformly f fun x => ∏' (i : ι), f i x
-- Mathlib.Logic.Function.Basic
Function.decidableEqPFun : (p : Prop) → [Decidable p] → (α : p → Type u_4) → [(hp : p) → DecidableEq (α hp)] → DecidableEq ((hp : p) → α hp)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.withInfoSyntaxFn : Lean.Parser.ParserFn → (Lean.SourceInfo → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- We can clear the denominators of a `Finset`-indexed family of fractions.  -/
IsLocalizedModule.exist_integer_multiples : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [IsLocalizedModule S f] {ι : Type u_4} (s : Finset ι) (g : ι → M'),
  ∃ b, ∀ i ∈ s, IsLocalizedModule.IsInteger f (↑b • g i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.diff_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁.diff m₂ ⋯).Equiv (m₁.diff m₃ ⋯)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.range_eq_top : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B), f.range = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_iSup : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra α),
  BooleanSubalgebra.map f (⨆ i, L i) = ⨆ i, BooleanSubalgebra.map f (L i)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterWithPostcondition.match_1.eq_2 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property { down := true })
  (h_1 : (h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩)
  (h_2 : (h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩),
  (match ⟨{ down := true }, h'⟩ with
    | ⟨{ down := false }, h'⟩ => h_1 h'
    | ⟨{ down := true }, h'⟩ => h_2 h') =
    h_2 h'
-- Mathlib.RingTheory.Ideal.Maps
FaithfulSMul.ker_algebraMap_eq_bot : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  RingHom.ker (algebraMap R A) = ⊥
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadInfo.mk.inj : ∀ {check : Lean.Elab.Term.Quotation.HeadCheck}
  {onMatch : Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.MatchResult}
  {doMatch :
    (List Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term → Lean.Elab.TermElabM Lean.Term}
  {check_1 : Lean.Elab.Term.Quotation.HeadCheck}
  {onMatch_1 : Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.MatchResult}
  {doMatch_1 :
    (List Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term → Lean.Elab.TermElabM Lean.Term},
  { check := check, onMatch := onMatch, doMatch := doMatch } =
      { check := check_1, onMatch := onMatch_1, doMatch := doMatch_1 } →
    check = check_1 ∧ onMatch = onMatch_1 ∧ doMatch = doMatch_1
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.sum : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ), ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = 1
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.State.mk.inj : ∀ {map : Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr} {set : Lean.PHashSet Lean.Meta.Sym.AlphaKey}
  {map_1 : Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr} {set_1 : Lean.PHashSet Lean.Meta.Sym.AlphaKey},
  { map := map, set := set } = { map := map_1, set := set_1 } → map = map_1 ∧ set = set_1
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.getRepr.match_1.eq_2 : ∀ {n : ℕ} (motive : Option (Fin n) → Sort u_1) (h_1 : (y : Fin n) → none = some y → motive (some y))
  (h_2 : none = none → motive none),
  (match h : none with
    | some y => h_1 y h
    | none => h_2 h) =
    h_2 ⋯
-- Std.Http.Internal.ChunkedBuffer
/-- The total size in bytes of all accumulated arrays
 -/
Std.Http.Internal.ChunkedBuffer.size : Std.Http.Internal.ChunkedBuffer → ℕ
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- The Gromov-Hausdorff distance can also be realized by a coupling in `ℓ^∞(ℝ)`, by embedding
the optimal coupling through its Kuratowski embedding.  -/
GromovHausdorff.ghDist_eq_hausdorffDist : ∀ (X : Type u) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] (Y : Type v)
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ GromovHausdorff.ghDist X Y = Metric.hausdorffDist (Set.range Φ) (Set.range Ψ)
-- Mathlib.Analysis.MellinTransform
/-- Predicate standing for "the Mellin transform of `f` is defined at `s` and equal to `m`". This
shortens some arguments.  -/
HasMellin : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℝ → E) → ℂ → E → Prop
-- Lean.Parser.Term
Lean.Parser.Term.letOptZeta.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.obj_η_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (n : M)
  (X : C) [inst_3 : F.Monoidal],
  (F.obj n).map ((CategoryTheory.Functor.OplaxMonoidal.η F).app X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit M) n).app X)
      ((F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor n).hom).app X)
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- A set of subsets of the vertices `V` of `G`.  -/
SimpleGraph.Partition.parts : {V : Type u} → {G : SimpleGraph V} → G.Partition → Set (Set V)
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.toFilterBasis : {A : Type u} → {inst : AddGroup A} → [self : AddGroupFilterBasis A] → FilterBasis A
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The modular discriminant is non-vanishing on the upper half-plane.  -/
ModularForm.discriminant_ne_zero : ∀ (z : UpperHalfPlane), ModularForm.discriminant z ≠ 0
-- Mathlib.RingTheory.HahnSeries.Summable
/-- The summation of a `summable_family` as a `LinearMap`.  -/
HahnSeries.SummableFamily.lsum : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      [inst : AddCommMonoid Γ] →
        [inst_1 : PartialOrder Γ] →
          [inst_2 : IsOrderedCancelAddMonoid Γ] →
            [inst_3 : Semiring R] → HahnSeries.SummableFamily Γ R α →ₗ[HahnSeries Γ R] HahnSeries Γ R
-- Mathlib.RingTheory.Fintype
ZMod.ringEquivOfPrime.congr_simp : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : Fintype R] {p : ℕ} (hp : Nat.Prime p) (hR : Fintype.card R = p),
  ZMod.ringEquivOfPrime R hp hR = ZMod.ringEquivOfPrime R hp hR
-- Mathlib.Topology.ContinuousOn
continuousOn_apply : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] (i : ι) (s : Set ((i : ι) → X i)),
  ContinuousOn (fun p => p i) s
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
/-- **Data processing inequality** for the Kullback-Leibler divergence and sub-sigma-algebras.  -/
InformationTheory.klDiv_trim_le : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} (μ ν : MeasureTheory.Measure 𝓧) [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] (hm : m ≤ m𝓧),
  InformationTheory.klDiv (μ.trim hm) (ν.trim hm) ≤ InformationTheory.klDiv μ ν
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.LFunction.eq_1 : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ),
  DirichletCharacter.LFunction χ s = ZMod.LFunction (⇑χ) s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k k' : α},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.filterMap f t) k = (Std.ExtDTreeMap.Const.get? t k).bind (f k')
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.congrHypothesisExceptionId : Lean.InternalExceptionId
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.brecOn.eq : ∀ {V : Type u} [inst : Quiver V] {a : V} {motive : (a_1 : V) → Quiver.Path a a_1 → Sort u_1} {a_1 : V}
  (t : Quiver.Path a a_1) (F_1 : (a_2 : V) → (t : Quiver.Path a a_2) → Quiver.Path.below t → motive a_2 t),
  Quiver.Path.brecOn t F_1 = F_1 a_1 t (Quiver.Path.brecOn.go t F_1).2
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mulAction : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (P : Submodule R M) → MulAction R (M ⧸ P)