mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Coinductive
/-- Generates a constructor for a coinductive predicate that corresponds to constructors
in the original `InductiveView`.

The process:
1. Takes the flat inductive constructor type
2. Fills recursive call parameters with the actual coinductive predicates
3. Converts to existential form using the equivalence lemma
4. Applies the unfolding rule to get the final constructor form
 -/
_private.Lean.Elab.Coinductive.0.Lean.Elab.Command.generateCoinductiveConstructor : Array Lean.InductiveVal → Lean.Syntax → ℕ → Lean.Name → Lean.ConstructorVal → Lean.Elab.TermElabM Unit
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.ofFn.go.eq_2 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (x_2 : 0 ≤ n), Array.ofFn.go✝ f acc 0 x_2 = acc
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.mem_units_of_val_mem_inv_val_mem : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : Mˣ}, ↑x ∈ S → ↑x⁻¹ ∈ S → x ∈ S.units
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology] (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData),
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_equiv_eq_comap_symm : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R ≃+* S)
  (K : NonUnitalSubring R), NonUnitalSubring.map (↑f) K = NonUnitalSubring.comap f.symm K
-- Init.Data.Ord.Vector
Vector.compare_eq_compare_toList : ∀ {α : Type u_1} {n : ℕ} [inst : Ord α] {a b : Vector α n}, compare a b = compare a.toList b.toList
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- A version of the **Gelfand-Mazur Theorem** over `ℝ`.

If a field `F` is a normed `ℝ`-algebra, then `F` is isomorphic as an `ℝ`-algebra
either to `ℝ` or to `ℂ`.  -/
NormedAlgebra.Real.nonempty_algEquiv_or : ∀ (F : Type u_2) [inst : NormedField F] [inst_1 : NormedAlgebra ℝ F], Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ)
-- Init.Data.Bool
Bool.toNat_false : false.toNat = 0
-- Mathlib.Algebra.Category.Grp.Ulift
AddGrpCat.instCreatesLimitsOfSizeUliftFunctor.eq_1 : AddGrpCat.instCreatesLimitsOfSizeUliftFunctor =
  {
    CreatesLimitsOfShape := fun {J} [CategoryTheory.Category.{w, u} J] =>
      { CreatesLimit := fun {x} => CategoryTheory.createsLimitOfFullyFaithfulOfPreserves } }
-- Plausible.DeriveShrinkable
/-- Deriving handler for `Shrinkable`  -/
_private.Plausible.DeriveShrinkable.0.Plausible.mkShrinkableInstanceHandler : Array Lean.Name → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.Analysis.BoxIntegral.Basic
/-- The integral of a nonnegative function w.r.t. a volume generated by a locally-finite measure is
nonnegative.  -/
BoxIntegral.integral_nonneg : ∀ {ι : Type u} {I : BoxIntegral.Box ι} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {g : (ι → ℝ) → ℝ},
  (∀ x ∈ BoxIntegral.Box.Icc I, 0 ≤ g x) →
    ∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ],
      0 ≤ BoxIntegral.integral I l g μ.toBoxAdditive.toSMul
-- Mathlib.Lean.Meta.CongrTheorems
_private.Mathlib.Lean.Meta.CongrTheorems.0.Lean.Meta.mkRichHCongr.withNewEqs.loop : Lean.Meta.FunInfo →
  {α : Type} →
    Array Lean.Expr →
      Array Lean.Expr →
        Array Bool →
          (Array Lean.Meta.CongrArgKind → Array (Option (Lean.Expr × Lean.Expr × Lean.Expr)) → Lean.MetaM α) →
            ℕ → Array Lean.Meta.CongrArgKind → Array (Option (Lean.Expr × Lean.Expr × Lean.Expr)) → Lean.MetaM α
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.continuous_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous ⇑DomAddAct.mk.symm
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Cfg.mk.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {inst : Inhabited Γ} {l : Option Λ} {var : σ} {Tape : Turing.Tape Γ}
  {l_1 : Option Λ} {var_1 : σ} {Tape_1 : Turing.Tape Γ},
  { l := l, var := var, Tape := Tape } = { l := l_1, var := var_1, Tape := Tape_1 } →
    l = l_1 ∧ var = var_1 ∧ Tape = Tape_1
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_top : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  [inst_3 : RingHomClass F R S], Ideal.comap f ⊤ = ⊤
-- Mathlib.Topology.Instances.Matrix
summable_matrix_transpose : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} {f : X → Matrix m n R}, Summable (fun x => (f x).transpose) L ↔ Summable f L
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.isLocal_single_iff_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C),
  (CategoryTheory.MorphismProperty.single f).isLocal Z ↔
    Function.Bijective fun g => CategoryTheory.CategoryStruct.comp f g
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The canonical isomorphism of triangles
`binaryProductTriangle X₁ X₂ ≅ binaryBiproductTriangle X₁ X₂`.  -/
CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (X₁ X₂ : C) →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] →
            CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂ ≅
              CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.is_mul_left_invariant_outerMeasure : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [inst_2 : Group G]
  [inst_3 : SeparatelyContinuousMul G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) = μ K) →
    ∀ (g : G) (A : Set G), μ.outerMeasure ((fun x => g * x) ⁻¹' A) = μ.outerMeasure A
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r_mul_r : ∀ {n : ℕ} (i j : ZMod n), DihedralGroup.r i * DihedralGroup.r j = DihedralGroup.r (i + j)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_ofList_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)}, (Std.ExtHashMap.ofList l).size ≤ l.length
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.hasAffineProperty : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsSeparated fun X x x_1 x_2 => X.IsSeparated
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
/-- An explicit form for the constant in the triangle removal lemma.

Note that this depends on `SzemerediRegularity.bound`, which is a tower-type exponential. This means
`triangleRemovalBound` is in practice absolutely tiny.

This definition is meant to be used for small values of `ε`, and in particular is junk for values
of `ε` greater than or equal to `1`. The junk value is chosen to be positive, so that
`0 < ε → 0 < triangleRemovalBound ε` regardless of whether `ε < 1` or not.  -/
SimpleGraph.triangleRemovalBound : ℝ → ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.isoCoproduct_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f],
  (CategoryTheory.Limits.biproduct.isoCoproduct f).hom =
    CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.Sigma.ι f)
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.unbounded_univ : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [Nontrivial E], ¬Bornology.IsBounded Set.univ
-- Init.WFExtrinsicFix
WellFounded.extrinsicFix_eq_fix : ∀ {α : Sort u_2} {C : α → Sort u_1} [inst : ∀ (a : α), Nonempty (C a)] {R : α → α → Prop}
  {F : (a : α) → ((a' : α) → R a' a → C a') → C a} (wf : WellFounded R) {a : α},
  WellFounded.extrinsicFix R F a = wf.fix F a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.uproj.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (i : ℕ) (var : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_9) (i_1 : ℕ)
  (var_1 : Lean.FVarId) (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_9),
  (Lean.Compiler.LCNF.LetValue.uproj i var h = Lean.Compiler.LCNF.LetValue.uproj i_1 var_1 h_1) =
    (i = i_1 ∧ var = var_1)
-- Init.System.ST
/-- Runs an `ST` computation, in which mutable state via `ST.Ref` is the only side effect.
 -/
runST : {α : Type} → ((σ : Type) → ST σ α) → α
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.instQuiver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → Quiver (CategoryTheory.Center C)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.domDomCongr_toMultilinearMap : ∀ {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : TopologicalSpace M₂]
  [inst_6 : TopologicalSpace M₃] {ι' : Type u_1} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun x => M₂) M₃),
  (ContinuousMultilinearMap.domDomCongr e f).toMultilinearMap = MultilinearMap.domDomCongr e f.toMultilinearMap
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.brecOn : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive : (a a_1 : s.Pos) → String.Slice.Pattern.Model.IsLongestMatchAtChain pat a a_1 → Prop} {a a_1 : s.Pos}
  (t : String.Slice.Pattern.Model.IsLongestMatchAtChain pat a a_1),
  (∀ (a a_2 : s.Pos) (t : String.Slice.Pattern.Model.IsLongestMatchAtChain pat a a_2),
      String.Slice.Pattern.Model.IsLongestMatchAtChain.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.Algebra.Category.Grp.Basic
/-- `Ab` is an abbreviation for `AddCommGrpCat`, for the sake of mathematicians' sanity.  -/
Ab : Type (u_1 + 1)
-- Aesop.Stats.Basic
Aesop.RuleStatsTotals.mk.inj : ∀ {numSuccessful numFailed : ℕ} {elapsedSuccessful elapsedFailed : Aesop.Nanos} {numSuccessful_1 numFailed_1 : ℕ}
  {elapsedSuccessful_1 elapsedFailed_1 : Aesop.Nanos},
  { numSuccessful := numSuccessful, numFailed := numFailed, elapsedSuccessful := elapsedSuccessful,
        elapsedFailed := elapsedFailed } =
      { numSuccessful := numSuccessful_1, numFailed := numFailed_1, elapsedSuccessful := elapsedSuccessful_1,
        elapsedFailed := elapsedFailed_1 } →
    numSuccessful = numSuccessful_1 ∧
      numFailed = numFailed_1 ∧ elapsedSuccessful = elapsedSuccessful_1 ∧ elapsedFailed = elapsedFailed_1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.cycles 0 ≅ K.homology 0` for a cochain complex `K`
indexed by `ℕ`.  -/
CochainComplex.isoHomologyπ₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (K : CochainComplex C ℕ) →
        [inst_2 : HomologicalComplex.HasHomology K 0] → HomologicalComplex.cycles K 0 ≅ HomologicalComplex.homology K 0
-- Mathlib.CategoryTheory.Localization.Adjunction
CategoryTheory.Adjunction.localization_unit_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁)
  [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂)
  [inst_5 : L₂.IsLocalization W₂] (G' : CategoryTheory.Functor D₁ D₂) (F' : CategoryTheory.Functor D₂ D₁)
  [inst_6 : CategoryTheory.CatCommSq G L₁ L₂ G'] [inst_7 : CategoryTheory.CatCommSq F L₂ L₁ F'] (X₁ : C₁),
  (adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) =
    CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁))
        (F'.map ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').hom.app X₁)))
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.irreducible_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] (r : R), Irreducible (Polynomial.X - Polynomial.C r)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.preimage_eball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : β)
  (r : ENNReal), ⇑h ⁻¹' Metric.eball x r = Metric.eball (h.symm x) r
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
/-- `sInf s < b` when there is an element `a` in `s` with `a < b`, when `s` is bounded below.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness below for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case.  -/
DirectedOn.csInf_lt_of_lt : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a b : α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → BddBelow s → a ∈ s → a < b → sInf s < b
-- Mathlib.Computability.MyhillNerode
Language.step_toDFA : ∀ {α : Type u} {L : Language α} (s : ↑(Set.range L.leftQuotient)) (a : α), ↑(L.toDFA.step s a) = (↑s).leftQuotient [a]
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).hom
      (CategoryTheory.Limits.colimit.ι F j).op =
    CategoryTheory.Limits.limit.π F.rightOp (Opposite.unop j)
-- Mathlib.Data.Rat.Defs
Rat.commSemigroup : CommSemigroup ℚ
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
CochainComplex.isoHomologyπ₀_inv_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℕ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomology K 0]
  [inst_3 : HomologicalComplex.HasHomology L 0] {Z : C} (h : HomologicalComplex.cycles L 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ 0)
      (CategoryTheory.CategoryStruct.comp L.isoHomologyπ₀.inv h) =
    CategoryTheory.CategoryStruct.comp K.isoHomologyπ₀.inv
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ 0) h)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.funLike : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → FunLike (L.Embedding M N) M N
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.minKey! ∈ t
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toCoalgHom_inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {e₁ e₂ : A ≃ₗc[R] B}, ↑e₁ = ↑e₂ ↔ e₁ = e₂
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.linearIndependent_restrict : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndepOn R v s → LinearIndependent (ι := ↑s) R (s.domRestrict v)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Topology.DiscreteSubset
/-- If `U` is closed and `s` is codiscrete within `U`, then `U \ s` is closed.  -/
isClosed_sdiff_of_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s U : Set X},
  s ∈ Filter.codiscreteWithin U → IsClosed U → IsClosed (U \ s)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.coe_mkContinuous : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] (f : MultilinearMap 𝕜 E G) (C : ℝ)
  (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖), ⇑(f.mkContinuous C H) = ⇑f
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_const_enorm : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [MeasureTheory.IsFiniteMeasure μ] {c : ε},
  ‖c‖ₑ ≠ ⊤ → MeasureTheory.Integrable (fun x => c) μ
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : X.Opens} {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (hV : AlgebraicGeometry.IsAffineOpen V) (i : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appLE f U V i))
      hU.fromSpec =
    CategoryTheory.CategoryStruct.comp hV.fromSpec f
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_dvd1_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → Bool
-- Init.Data.Int.Gcd
Int.gcd_mul_right_sub_left : ∀ (m n k : ℤ), (k * m - n).gcd m = n.gcd m
-- Mathlib.RingTheory.Norm.Transitivity
/-- The lower-right corner of `M * aux M k` is the same as the corner of `M`.  -/
Algebra.Norm.Transitivity.mul_auxMat_corner : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m)
  [inst_2 : Fintype m], (M * Algebra.Norm.Transitivity.auxMat M k) k k = M k k
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.sup_aeval_range_eq_top_of_isCoprime : ∀ {R : Type u} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M →ₗ[R] M)
  {p q : Polynomial R}, IsCoprime p q → ((Polynomial.aeval f) p).range ⊔ ((Polynomial.aeval f) q).range = ⊤
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.smuld_val : ∀ {d : ℤ} (n x y : ℤ), Zsqrtd.sqrtd * ↑n * { re := x, im := y } = { re := d * n * y, im := n * x }
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder : ∀ {p : ℝ} [hp : Fact (0 < p)] {u : AddCircle p}, IsOfFinAddOrder u → u ≠ 0 → p ≤ addOrderOf u • ‖u‖
-- Mathlib.Data.Set.Image
Set.powerset_insert_injOn : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → Set.InjOn (insert a) (𝒫 s)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.mk.inj : ∀ {α : Type} {state state_1 : Std.Mutex (Std.CloseableChannel.Unbounded.State✝ α)},
  { state := state } = { state := state_1 } → state = state_1
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_refl : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R), x ≤ᵥ x
-- Mathlib.Data.List.Palindrome
List.Palindrome.below.nil : ∀ {α : Type u_1} {motive : (a : List α) → a.Palindrome → Prop}, List.Palindrome.below ⋯
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  IsLocalization.mk' S x y = (IsLocalization.toLocalizationMap M S).mk' x y
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_mem_nhdsSet : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (E : Set α) {δ : ℝ}, 0 < δ → Metric.cthickening δ E ∈ nhdsSet E
-- Mathlib.Analysis.Analytic.IsolatedZeros
AnalyticAt.frequently_eq_iff_eventually_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    AnalyticAt 𝕜 g z₀ → ((∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) ↔ ∀ᶠ (z : 𝕜) in nhds z₀, f z = g z)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.pair_comm : ∀ {α : Type u_1} (x y : α), {x, y} = {y, x}
-- Mathlib.Order.Atoms
isAtomic_of_isCoatomic_of_complementedLattice_of_isModular : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] [ComplementedLattice α]
  [IsCoatomic α], IsAtomic α
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- A submodule of a free `R`-module of finite rank is also a free `R`-module of finite rank,
if `R` is a principal ideal domain.

See also the stronger version `Submodule.smithNormalForm`.
 -/
Submodule.basisOfPid : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [IsPrincipalIdealRing R] →
            [IsDomain R] →
              {ι : Type u_4} →
                [Finite ι] → Module.Basis ι R M → (N : Submodule R M) → (n : ℕ) × Module.Basis (Fin n) R ↥N
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.isEmpty = true → (t.insertIfNew k v).minKey ⋯ = k
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.BiconeMorphism.mk.injEq : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
  (hom : A.pt ⟶ B.pt)
  (wπ :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π j) = A.π j)
      CategoryTheory.Limits.BiconeMorphism.wπ._autoParam)
  (wι :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) hom = B.ι j)
      CategoryTheory.Limits.BiconeMorphism.wι._autoParam)
  (hom_1 : A.pt ⟶ B.pt)
  (wπ_1 :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom_1 (B.π j) = A.π j)
      CategoryTheory.Limits.BiconeMorphism.wπ._autoParam)
  (wι_1 :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) hom_1 = B.ι j)
      CategoryTheory.Limits.BiconeMorphism.wι._autoParam),
  ({ hom := hom, wπ := wπ, wι := wι } = { hom := hom_1, wπ := wπ_1, wι := wι_1 }) = (hom = hom_1)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {U : CategoryTheory.Comonad C} {of of_1 : C},
  { of := of } = { of := of_1 } → of = of_1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : D} (S : CategoryTheory.Sieve X) (e : C ≌ D),
  CategoryTheory.Sieve.functorPushforward e.inverse S =
    CategoryTheory.Sieve.functorPullback e.functor (CategoryTheory.Sieve.pullback (e.counit.app X) S)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- When `P : ObjectProperty C` is monoidal, the full subcategory for `P` inherits the
monoidal structure of `C`.
 -/
CategoryTheory.ObjectProperty.fullMonoidalSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (P : CategoryTheory.ObjectProperty C) → [P.IsMonoidal] → CategoryTheory.MonoidalCategory P.FullSubcategory
-- Mathlib.Combinatorics.Colex
Finset.Colex.IsInitSeg.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (𝒜 : Finset (Finset α)) (r : ℕ),
  Finset.Colex.IsInitSeg 𝒜 r = (Set.Sized r ↑𝒜 ∧ ∀ ⦃s t : Finset α⦄, s ∈ 𝒜 → toColex t < toColex s ∧ t.card = r → t ∈ 𝒜)