mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.GroupWithZero.Basic
/-- In a monoid with zero, if zero equals one, then zero is the only element.  -/
eq_zero_of_zero_eq_one : ∀ {M₀ : Type u_1} [inst : MulZeroOneClass M₀], 0 = 1 → ∀ (a : M₀), a = 0
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.coeff_mapAlgHom : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B)
  (x : MonoidAlgebra A M) (m : M), ((MonoidAlgebra.mapAlgHom M f) x).coeff m = f (x.coeff m)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.meromorphicOn_comp_sub_const_iff_meromorphicOn`

---

`MeromorphicOn` is invariant under translation.  -/
MeromorphicOn.meromorphicOn_fun_comp_sub_const_iff_meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {U : Set 𝕜},
  MeromorphicOn (fun x => f (x - c)) U ↔ MeromorphicOn f (U - {c})
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.subtype_injective : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.ElementarySubstructure M),
  Function.Injective ⇑S.subtype
-- Init.Data.List.Lemmas
List.nil_eq : ∀ {α : Type u_1} {xs : List α}, [] = xs ↔ xs = []
-- Mathlib.Topology.Irreducible
IsDiscrete.subsingleton_of_isPreirreducible : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → IsPreirreducible s → s.Subsingleton
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.isEmpty = (t.size == 0)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ringHom_ext'_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] [inst_2 : Semiring S]
  {f g : MonoidAlgebra R M →+* S},
  f = g ↔
    f.comp MonoidAlgebra.singleOneRingHom = g.comp MonoidAlgebra.singleOneRingHom ∧
      (↑f).comp (MonoidAlgebra.of R M) = (↑g).comp (MonoidAlgebra.of R M)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.forgetStalk_hom_comp_evalHom : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)),
  CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).hom (smoothSheaf.evalHom IM I R x) =
    TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.evalHom IM I M R x))
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_sInf : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {S : Set (NonUnitalSubsemiring R)} {x : R},
  x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Init.Data.List.Lemmas
List.partition.loop.eq_1 : ∀ {α : Type u} (p : α → Bool) (bs cs : List α), List.partition.loop p [] (bs, cs) = (bs.reverse, cs.reverse)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_basis_equiv : ∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Fintype l]
  [inst_6 : DecidableEq l] (b : Module.Basis l R M₁) (b' : Module.Basis l R M₂),
  (LinearMap.toMatrix b' b) ↑(b'.equiv b (Equiv.refl l)) = 1
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- The sheafification of a presheaf `P`, as a functor.
*NOTE:* Additional hypotheses are needed to obtain a proof that this is a sheaf!  -/
CategoryTheory.GrothendieckTopology.sheafification : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor Cᵒᵖ D)
-- Std.Time.Format.Modifier
Std.Time.instInhabitedOffsetX.default : Std.Time.OffsetX
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_inv_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] (x : C) {Z : V}
  (h : (CategoryTheory.MonoidalCategory.DayConvolution.convolution U F).obj x ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F).inv.app x) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj x)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.DayConvolutionUnit.can
          (F.obj x))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit U F).app
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C, x))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.MonoidalCategory.DayConvolution.convolution U F).map
              (CategoryTheory.MonoidalCategoryStruct.leftUnitor x).hom)
            h)))
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.ofDirectSum_toDirectSum : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (x : TensorAlgebra R M), TensorAlgebra.ofDirectSum (TensorAlgebra.toDirectSum x) = x
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
/-- The exponential comparison map.
`F` is a Cartesian closed functor if this is an iso for all `A`.
 -/
CategoryTheory.expComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} D] →
        [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : CategoryTheory.MonoidalClosed C] →
                [inst_5 : CategoryTheory.MonoidalClosed D] →
                  [CategoryTheory.Limits.PreservesLimitsOfShape
                        (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] →
                    (A : C) → CategoryTheory.TwoSquare (CategoryTheory.ihom A) F F (CategoryTheory.ihom (F.obj A))
-- Mathlib.Analysis.Normed.Ring.Basic
SubringClass.toSeminormedRing : {S : Type u_5} →
  {R : Type u_6} → [inst : SetLike S R] → [inst_1 : SeminormedRing R] → [SubringClass S R] → (s : S) → SeminormedRing ↥s
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_of_veq_of_vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x =ᵥ y → y ≤ᵥ z → x ≤ᵥ z
-- Mathlib.Topology.Order.Compact
IsCompact.isLUB_sSup : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIciTopology α]
  {s : Set α}, IsCompact s → s.Nonempty → IsLUB s (sSup s)
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.rotateR.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → Sort u_2) (y : α) (r : Ordnode α)
  (h_1 :
    (size : ℕ) →
      (l : Ordnode α) → (x : α) → (m : Ordnode α) → (y : α) → (r : Ordnode α) → motive (Ordnode.node size l x m) y r)
  (h_2 : (y : α) → (r : Ordnode α) → motive Ordnode.nil y r),
  (match Ordnode.nil, y, r with
    | Ordnode.node size l x m, y, r => h_1 size l x m y r
    | Ordnode.nil, y, r => h_2 y r) =
    h_2 y r
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- The square of `f.normDet` equals the determinant of `f.adjoint ∘ₗ f` when the codomain is finite
dimensional.
 -/
LinearMap.normDet_sq : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] [inst_6 : FiniteDimensional 𝕜 V] (f : U →ₗ[𝕜] V),
  ↑(f.normDet ^ 2) = LinearMap.det (LinearMap.adjoint f ∘ₗ f)
-- Mathlib.Topology.Separation.Hausdorff
/-- Retract subspaces of Hausdorff spaces are closed.  -/
Function.LeftInverse.isClosed_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space X] {f : X → Y}
  {g : Y → X}, Function.LeftInverse f g → Continuous f → Continuous g → IsClosed (Set.range g)
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_smul_eq_comap : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure]
  [μ.Regular] (φ : G ≃ₜ+ G), MeasureTheory.addEquivAddHaarChar φ • μ = MeasureTheory.Measure.comap (⇑φ) μ
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_C_mul_X_pow_subset : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (c : R), (Polynomial.C c * Polynomial.X ^ n).support ⊆ {n}
-- Mathlib.Data.Fin.Tuple.Basic
/-- `Fin.find p h` returns the smallest index `k : Fin n` where `p k` is satisfied,
given that it is satisfied for some `k`.  -/
Fin.find : {n : ℕ} → (p : Fin n → Prop) → [DecidablePred p] → (∃ k, p k) → Fin n
-- Mathlib.Order.Monotone.Defs
antitone_iff_apply₂ : ∀ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [inst : (i : ι) → Preorder (β i)] [inst_1 : Preorder α]
  {f : α → (i : ι) → β i}, Antitone f ↔ ∀ (i : ι), Antitone fun x => f x i
-- Init.Internal.Order.Basic
/-- The main fixpoint theorem for fixed points of monotone functions in chain-complete partial orders.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.fix_eq : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {f : α → α} (hf : Lean.Order.monotone f),
  Lean.Order.fix f hf = f (Lean.Order.fix f hf)
-- Mathlib.Analysis.Complex.Poisson
/-- **Poisson integral formula** for ℂ-differentiable functions on arbitrary disks in the complex plane,
formulated with the real part of the Herglotz–Riesz kernel of integration expanded.
 -/
DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {R : ℝ} {w : ℂ} [CompleteSpace E]
  {c : ℂ},
  DiffContOnCl ℂ f (Metric.ball c R) →
    w ∈ Metric.ball c R → Real.circleAverage (fun z => ((z - c + (w - c)) / (z - c - (w - c))).re • f z) c R = f w
-- Mathlib.Algebra.Category.CoalgCat.Basic
CategoryTheory.Iso.toCoalgEquiv_trans : ∀ {R : Type u} [inst : CommRing R] {X Y Z : CoalgCat R} (e : X ≅ Y) (f : Y ≅ Z),
  (e ≪≫ f).toCoalgEquiv = e.toCoalgEquiv.trans f.toCoalgEquiv
-- Mathlib.Data.Rat.Floor
Rat.isNat_intFract_of_isNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] (r : R)
  (m : ℕ), Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat (Int.fract r) 0
-- Batteries.Recycling.RBTree.Basic
/-- The predicate asserting that the result of `modifyP` is safe to construct.  -/
RBTree.RBSet.ModifyWF : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Ordering) → (α → α) → Prop
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.i.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L),
  CochainComplex.cm5b.i f =
    CategoryTheory.Limits.biprod.lift
      (CochainComplex.mappingCone.lift (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))
        (CochainComplex.HomComplex.Cocycle.mk
          (CochainComplex.HomComplex.Cochain.mk fun p q x =>
            CategoryTheory.CategoryStruct.comp (K.d p q) (CategoryTheory.Injective.ι (K.X q)))
          2 CochainComplex.cm5b.i._proof_2 ⋯)
        (CochainComplex.HomComplex.Cochain.ofHoms fun n => CategoryTheory.Injective.ι (K.X n)) ⋯)
      f
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The category `SimplicialObject.Split C` is the category of simplicial objects
in `C` equipped with a splitting, and morphisms are morphisms of simplicial objects
which are compatible with the splittings.  -/
CategoryTheory.SimplicialObject.Split : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max u_1 v_1)
-- Init.Data.Int.Linear
/-- Returns the constant of the given linear polynomial.  -/
Int.Internal.Linear.Poly.getConst : Int.Internal.Linear.Poly → ℤ
-- Mathlib.Topology.Inseparable
/-- **Alias** of `GeneralizingMap.stableUnderGeneralization_image`. -/
StableUnderGeneralization.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  GeneralizingMap f → ∀ {s : Set X}, StableUnderGeneralization s → StableUnderGeneralization (f '' s)
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A constructor for chain maps between `ℕ`-indexed cochain complexes,
working by induction on commutative squares.

You need to provide the components of the chain map in degrees 0 and 1,
show that these form a commutative square,
and then give a construction of each component,
and the fact that it forms a commutative square with the previous component,
using as an inductive hypothesis the data (and commutativity) of the previous two components.
 -/
CochainComplex.mkHom : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (P Q : CochainComplex V ℕ) →
        (zero : P.X 0 ⟶ Q.X 0) →
          (one : P.X 1 ⟶ Q.X 1) →
            CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one →
              ((n : ℕ) →
                  (p :
                      (f : P.X n ⟶ Q.X n) ×'
                        (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
                          CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                            CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') →
                    (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
                      CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) =
                        CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'') →
                (P ⟶ Q)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- A strong epi category is a category in which every epimorphism is strong.  -/
CategoryTheory.StrongEpiCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (s : ℤˣ), s ^ 0 = 1
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.State.mk : Std.Format → ℕ → List (ℕ × Std.Format) → Lean.PrettyPrinter.OneLine.State
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformly.summable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {x : β}
  [inst_1 : UniformSpace α], SummableUniformly f → Summable fun x_1 => f x_1 x
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.GetElem?.match_1.splitter : (elem : outParam (Type u_1)) →
  (motive : Option elem → Sort u_2) →
    (x : Option elem) → ((e : elem) → motive (some e)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry'_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.Closed X] [inst_3 : CategoryTheory.Closed Y] (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.MonoidalClosed.curry' (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalClosed.curry' f)
          (CategoryTheory.MonoidalClosed.curry' g))
        (CategoryTheory.MonoidalClosed.comp X Y Z))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instSMulCommClass : ∀ {α : Type u_1} {R : Type u_6} {R' : Type u_7} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal]
  [inst_2 : SMul R' ENNReal] [inst_3 : IsScalarTower R' ENNReal ENNReal] [SMulCommClass R R' ENNReal]
  {x : MeasurableSpace α}, SMulCommClass R R' (MeasureTheory.Measure α)
-- Mathlib.Logic.Equiv.Embedding
_private.Mathlib.Logic.Equiv.Embedding.0.Equiv.sumEmbeddingEquivProdEmbeddingDisjoint.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (b : β) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (b : β) → motive (Sum.inr b)),
  (match Sum.inr b with
    | Sum.inl a => h_1 a
    | Sum.inr b => h_2 b) =
    h_2 b
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.unifTight_iff_ennreal : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : NormedAddCommGroup β] {x : MeasurableSpace α} (f : ι → α → β)
  (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.UnifTight f p μ ↔
    ∀ ⦃ε : ENNReal⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), MeasureTheory.eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε
-- Mathlib.Order.FixedPoints
OrderHom.gfp_le_map : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, OrderHom.gfp f ≤ a → OrderHom.gfp f ≤ f a
-- Lean.Level
Lean.instInhabitedLevel : Inhabited Lean.Level
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.coe_of : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] [inst_3 : CompactSpace G]
  [inst_4 : TotallyDisconnectedSpace G], ↑(ProfiniteGrp.of G).toProfinite.toTop = G
-- Init.System.IO
/-- A new file should be created for writing.

It is an error if the file already exists. A new file is created, with the read/write cursor
positioned at the start.

* `open` flags: `O_WRONLY | O_CREAT | O_TRUNC | O_EXCL`
* `fdopen` mode: `w`
 -/
IO.FS.Mode.writeNew : IO.FS.Mode
-- Mathlib.Data.Fin.Rev
/-- `rev` commutes with `predAbove`.  -/
Fin.rev_predAbove : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)), (p.predAbove i).rev = p.rev.predAbove i.rev
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
IsIntegral.isAlmostIntegral_of_exists_smul_mem_range : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {s : S},
  IsIntegral R s → (∃ t ∈ nonZeroDivisors R, t • s ∈ (algebraMap R S).range) → IsAlmostIntegral R s
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.maxEntry : {α : Type u} → {β : α → Type v} → (t : Std.DTreeMap.Internal.Impl α β) → t.isEmpty = false → (a : α) × β a
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.wellPowered : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.WellPowered.{w, v, u} C
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
self_le_mul_right : ∀ {α : Type u} [inst : Mul α] [inst_1 : LE α] [CanonicallyOrderedMul α] (a b : α), a ≤ a * b
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.fixedBy_one_eq_univ : ∀ (α : Type u_1) (M : Type u_3) [inst : Monoid M] [inst_1 : MulAction M α], MulAction.fixedBy α 1 = Set.univ
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n')
  (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'),
  (CochainComplex.HomComplex.Cochain.leftShiftAddEquiv K L n a n' hn').symm γ = γ.leftUnshift n hn'
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.State.mk.inj : ∀ {cache : Std.HashSet (Option Lean.Expr × Lean.Expr × Bool)} {progress : Mathlib.Tactic.GRewrite.Progress✝}
  {cache_1 : Std.HashSet (Option Lean.Expr × Lean.Expr × Bool)} {progress_1 : Mathlib.Tactic.GRewrite.Progress✝},
  { cache := cache, progress := progress } = { cache := cache_1, progress := progress_1 } →
    cache = cache_1 ∧ progress = progress_1
-- Mathlib.Topology.MetricSpace.UniformConvergence
/-- If `f : α → γ → β` is a family of a functions, all of which are Lipschitz with the
same constant, then the family is uniformly equicontinuous.  -/
LipschitzWith.uniformEquicontinuous : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] [inst_1 : PseudoEMetricSpace β]
  (f : α → γ → β) (K : NNReal), (∀ (c : α), LipschitzWith K (f c)) → UniformEquicontinuous f
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.radical_mul : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData}, (I * J).radical = I.radical ⊓ J.radical
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.I_im : UpperHalfPlane.I.im = 1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_congr : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε},
  Set.EqOn f g (Set.uIoc a b) → (IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b)
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fg_iff_addSubmonoid_fg : ∀ {M : Type u_1} [inst : AddMonoid M] (N : AddSubmonoid M), AddMonoid.FG ↥N ↔ N.FG
-- Mathlib.Order.Minimal
MaximalFor.not_gt : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {Q : ι → Prop} {f : ι → α} {i j : ι},
  MaximalFor Q f i → Q j → ¬f i < f j