mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_erase_eq_of_not_compare_minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k fallback : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ¬compare k (t.minKeyD fallback) = Ordering.eq →
      (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKeyD fallback = t.minKeyD fallback
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- Generate a "simp only [...]" suggestion for a simp/simpAll tactic.
Returns `none` if the tactic is not simp/simpAll or if suggestion generation fails.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.generateSimpSuggestion : Mathlib.Linter.Flexible.StainData✝ → Lean.Syntax → Lean.CoreM (Option Lean.Syntax)
-- Mathlib.Topology.Constructions
IsClosedMap.codRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsClosedMap f → ∀ {s : Set Y} (hs : ∀ (a : X), f a ∈ s), IsClosedMap (Set.codRestrict f s hs)
-- Init.Data.Option.Basic
Option.any_none : ∀ {α : Type u_1} {p : α → Bool}, Option.any p none = false
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.single_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ L.X q) (n : ℤ) (hpq : p + n = q),
  (CochainComplex.HomComplex.Cochain.single f n).v p q hpq = f
-- Lean.Elab.InfoTree.Main
Lean.Elab.enableInfoTree : {m : Type → Type} → [Lean.Elab.MonadInfoTree m] → optParam Bool true → m Unit
-- Mathlib.Topology.Order.LeftRight
frequently_gt_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] (a : α) [(nhdsWithin a (Set.Ioi a)).NeBot],
  ∃ᶠ (x : α) in nhds a, a < x
-- Mathlib.Data.Set.Pairwise.Lattice
Set.biUnionEqSigmaOfDisjoint.eq_1 : ∀ {α : Type u_1} {ι : Type u_2} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f),
  Set.biUnionEqSigmaOfDisjoint h = (Equiv.setCongr ⋯).trans (Set.unionEqSigmaOfDisjoint ⋯)
-- Mathlib.Logic.Relation
Relation.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (r : α → β → Prop)
  (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → ζ),
  Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_eq_measure_smaller_of_between_null_sdiff`. -/
MeasureTheory.measure_eq_measure_smaller_of_between_null_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ (s₃ \ s₁) = 0 → μ s₁ = μ s₂
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The normal subgroups correspond to the congruence relations on a group.
 -/
Subgroup.orderIsoCon : {G : Type u_1} → [inst : Group G] → { N // N.Normal } ≃o Con G
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.isUnit_iff_eq_one : ∀ {M : Type u_1} [inst : CommMonoid M] (a : Associates M), IsUnit a ↔ a = 1
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_lt_mul_of_neg_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b c : R} [ExistsAddOfLE R] [PosMulStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R], b < a → c < 0 → c * a < c * b
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.descFunLift.eq_3 : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat)
  (s : CategoryTheory.Limits.Cocone F) (x_1 y : MonCat.Colimits.Prequotient F),
  MonCat.Colimits.descFunLift F s (x_1.mul y) = MonCat.Colimits.descFunLift F s x_1 * MonCat.Colimits.descFunLift F s y
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.apply_skipPrefixWhile_bool_eq_false : ∀ {p : Char → Bool} {s : String.Slice} {h : s.skipPrefixWhile p ≠ s.endPos}, p ((s.skipPrefixWhile p).get h) = false
-- Mathlib.CategoryTheory.Sites.Sieves
/-- When `F` is essentially surjective and full, the Galois connection is a Galois insertion.  -/
CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.EssSurj] →
            [F.Full] →
              (X : C) →
                GaloisInsertion (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
-- Lean.Elab.App
/-- Returns the current parameter's type.
Only valid if `fTypeIsForall` has returned `true`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getParamType : Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Around a point in the target, `(extChartAt I x).target` and `range I` coincide locally.  -/
extChartAt_target_eventuallyEq_of_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M} {z : E},
  z ∈ (extChartAt I x).target → (extChartAt I x).target =ᶠ[nhds z] Set.range ↑I
-- Mathlib.Algebra.Polynomial.RuleOfSigns
_private.Mathlib.Algebra.Polynomial.RuleOfSigns.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.Defs.0.Std.DHashMap.Internal.Raw₀.expand.go.induct : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α]
  (motive : ℕ → Array (Std.DHashMap.Internal.AssocList α β) → { d // 0 < d.size } → Prop),
  (∀ (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β)) (target : { d // 0 < d.size })
      (h : i < source.size),
      have es := source[i];
      have source_1 := source.set i Std.DHashMap.Internal.AssocList.nil h;
      have target_1 := Std.DHashMap.Internal.AssocList.foldl (Std.DHashMap.Internal.Raw₀.reinsertAux hash) target es;
      motive (i + 1) source_1 target_1 → motive i source target) →
    (∀ (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β)) (target : { d // 0 < d.size }),
        ¬i < source.size → motive i source target) →
      ∀ (i : ℕ) (source : Array (Std.DHashMap.Internal.AssocList α β)) (target : { d // 0 < d.size }),
        motive i source target
-- Mathlib.Analysis.Calculus.Implicit
ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : CompleteSpace E] [inst_8 : CompleteSpace (F × G)]
  (f f_1 : E →L[𝕜] F) (e_f : f = f_1) (g g_1 : E →L[𝕜] G) (e_g : g = g_1) (hf : (↑f).range = ⊤) (hg : (↑g).range = ⊤)
  (hfg : IsCompl (↑f).ker (↑g).ker),
  f.equivProdOfSurjectiveOfIsCompl g hf hg hfg = f_1.equivProdOfSurjectiveOfIsCompl g_1 ⋯ ⋯ ⋯
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldrM.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (x : δ) (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldrM f x (Std.DHashMap.Internal.AssocList.cons a b es) = do
    let d ← Std.DHashMap.Internal.AssocList.foldrM f x es
    f a b d
-- Mathlib.Util.Notation3
/-- Create a `Term` that represents a matcher for `foldl` notation.
Reminder: `( lit ","* => foldl (x y => scopedTerm) init)`  -/
Mathlib.Notation3.mkFoldlMatcher : Lean.Name →
  Lean.Name →
    Lean.Name →
      Lean.Term →
        Lean.Term → Array Lean.Name → OptionT Lean.Elab.TermElabM (List Mathlib.Notation3.DelabKey × Lean.Term)
-- Mathlib.Algebra.Algebra.Basic
algebraMap_comp_natCast : ∀ (R : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ⇑(algebraMap R A) ∘ Nat.cast = Nat.cast
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_eq_sSup : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (f : ℝ →+*o K) (x : K),
  ArchimedeanClass.stdPart x = sSup {r | f r < x}
-- Init.WF
WellFounded.Nat.fix.go.congr_simp : ∀ {α : Sort u} {motive : α → Sort v} (h : α → ℕ)
  (F F_1 : (x : α) → ((y : α) → InvImage (fun x1 x2 => x1 < x2) h y x → motive y) → motive x),
  F = F_1 →
    ∀ (fuel fuel_1 : ℕ) (e_fuel : fuel = fuel_1) (x : α) (a : h x < fuel),
      WellFounded.Nat.fix.go h F fuel x a = WellFounded.Nat.fix.go h F_1 fuel_1 x ⋯
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
hasSum_nat_jacobiTheta : ∀ {τ : ℂ}, 0 < τ.im → HasSum (fun n => Complex.exp (↑Real.pi * Complex.I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
-- Std.Sat.AIG.Lemmas
/-- If an index contains a `Decl.gate` we know how to denote it.
 -/
Std.Sat.AIG.denote_idx_gate : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {start : ℕ} {assign : α → Bool} {invert : Bool}
  {lhs rhs : Std.Sat.AIG.Fanin} {aig : Std.Sat.AIG α} {hstart : start < aig.decls.size}
  (h : aig.decls[start] = Std.Sat.AIG.Decl.gate lhs rhs),
  ⟦assign, { aig := aig, ref := { gate := start, invert := invert, hgate := hstart } }⟧ =
    (⟦assign, { aig := aig, ref := { gate := lhs.gate, invert := lhs.invert, hgate := ⋯ } }⟧ &&
        ⟦assign, { aig := aig, ref := { gate := rhs.gate, invert := rhs.invert, hgate := ⋯ } }⟧ ^^
      invert)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Fintype.prod_empty : ∀ {ι : Type u_1} {M : Type u_3} [inst : Fintype ι] [inst_1 : CommMonoid M] [IsEmpty ι] (f : ι → M), ∏ x, f x = 1
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The unique map from the head to the pushout.  -/
CategoryTheory.Limits.WidePushout.head : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {B : C} →
        {objs : J → C} →
          (arrows : (j : J) → B ⟶ objs j) →
            [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] →
              B ⟶ CategoryTheory.Limits.widePushout B objs arrows
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {f : BoundedLatticeHom α β}
  {a : α} {L : BooleanSubalgebra β}, a ∈ BooleanSubalgebra.comap f L ↔ f a ∈ L
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.DiscreteTopology.metrizableSpace : ∀ {X : Type u_2} [inst : TopologicalSpace X] [DiscreteTopology X], TopologicalSpace.MetrizableSpace X
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- If `G` preserves binary products and `C` has them, then the binary fan constructed of the mapped
morphisms of the binary product cone is a limit.
 -/
CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X Y : C) →
            [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] →
              [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] →
                CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Limits.BinaryFan.mk (G.map CategoryTheory.Limits.prod.fst)
                    (G.map CategoryTheory.Limits.prod.snd))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {l : List α}
  {k : α}, k ∈ t → (t.insertMany l).get! k = t.get! k
-- Init.Data.Int.Gcd
Int.gcd_sub_right_right_of_dvd : ∀ {n k : ℤ} (m : ℤ), n ∣ k → n.gcd (m - k) = n.gcd m
-- Mathlib.CategoryTheory.Types.Basic
/-- Turn a morphism in `Type` back into a function.  -/
TypeCat.Hom.hom : {X Y : Type u} → TypeCat.Hom X Y → TypeCat.Fun X Y
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orImpL.sizeOf_spec : ∀ (p : Mathlib.Tactic.ITauto.Proof), sizeOf p.orImpL = 1 + sizeOf p
-- Mathlib.RingTheory.Algebraic.Integral
/-- If `R` is a domain and `S` is an arbitrary `R`-algebra, then the elements of `S`
that are algebraic over `R` form a subalgebra.  -/
Subalgebra.algebraicClosure : (R : Type u_1) →
  (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → [IsDomain R] → Subalgebra R S
-- Mathlib.Analysis.InnerProductSpace.Continuous
Dense.eq_of_inner_right : ∀ {E : Type u_4} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E} {S : Set E}, Dense S → (∀ v ∈ S, inner 𝕜 v x = inner 𝕜 v y) → x = y
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {f g : 𝕜 → F},
        ContDiffWithinAt 𝕜 (↑n) f s x →
          ContDiffWithinAt 𝕜 (↑n) g s x →
            iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `K` and `Kᗮ` have trivial intersection.  -/
Submodule.orthogonal_disjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), Disjoint K Kᗮ
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_def : ∀ {α : Type u_4} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  MeasureTheory.lintegral μ f = ⨆ g, ⨆ (_ : ⇑g ≤ f), g.lintegral μ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.WalkingMultispan.functorExt.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MultispanShape} (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) (i : J.L)
  (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right i)),
  (match CategoryTheory.Limits.WalkingMultispan.left i with
    | CategoryTheory.Limits.WalkingMultispan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMultispan.right i => h_2 i) =
    h_1 i
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.X_pow : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).Splits
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuousAt_const_mul : ∀ {a b : ENNReal}, a ≠ ⊤ ∨ b ≠ 0 → ContinuousAt (fun x => a * x) b
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₅_app_three : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_449✝ ⟶ g.obj' 0 _proof_449✝) (app₁ : f.obj' 1 _proof_450✝ ⟶ g.obj' 1 _proof_450✝)
  (app₂ : f.obj' 2 _proof_451✝ ⟶ g.obj' 2 _proof_451✝) (app₃ : f.obj' 3 _proof_452✝ ⟶ g.obj' 3 _proof_452✝)
  (app₄ : f.obj' 4 _proof_453✝ ⟶ g.obj' 4 _proof_453✝) (app₅ : f.obj' 5 _proof_454✝ ⟶ g.obj' 5 _proof_454✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
      _auto_491✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_451✝))
      _auto_493✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_452✝))
      _auto_495✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_453✝))
      _auto_497✝)
  (w₄ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅ =
        CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_453✝ _proof_454✝))
      _auto_499✝),
  (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app
      ⟨3, CategoryTheory.ComposableArrows.homMk₅._proof_4⟩ =
    app₃
-- Init.Data.BitVec.Lemmas
BitVec.reverse.eq_1 : ∀ (x_2 : BitVec 0), x_2.reverse = x_2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Real.sinh_eq_tsum : ∀ (r : ℝ), Real.sinh r = ∑' (n : ℕ), r ^ (2 * n + 1) / ↑(2 * n + 1).factorial
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.Hom.mk.congr_simp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] {F : C → D}
  {P : CategoryTheory.MorphismProperty D} [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.InducedWideCategory D F P}
  (hom hom_1 : F X ⟶ F Y) (e_hom : hom = hom_1) (property : P hom),
  { hom := hom, property := property } = { hom := hom_1, property := ⋯ }
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.le_nhds : ∀ {a : outParam ℝ} (outer : Filter ℝ) {inner : outParam (Filter ℝ)} [self : intervalIntegral.FTCFilter a outer inner],
  inner ≤ nhds a
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for `tensorUnit`, the two-sided identity of `⊗`  -/
CategoryTheory.MonoidalCategory.«term𝟙__» : Lean.ParserDescr
-- Mathlib.Analysis.Real.Sqrt
/-- Extension for the `positivity` tactic: a square root of a strictly positive nonnegative real is
positive.  -/
Mathlib.Meta.Positivity.evalNNRealSqrt : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.tail_cons : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (a : Γ) (l : Turing.ListBlank Γ), (Turing.ListBlank.cons a l).tail = l
-- Mathlib.Order.SuccPred.Limit
Order.isPredLimitRecOn_pred_of_not_isMin : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  (isMax : (a : α) → IsMax a → motive a) (pred : (a : α) → ¬IsMin a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → motive a) (hb : ¬IsMin b),
  Order.isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isSeparating_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ),
  P.unop.IsSeparating ↔ P.IsCoseparating
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.get?ₘ_eq_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [inst_4 : Std.LawfulBEqOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.get?ₘ k = Std.Internal.List.getValueCast? k t.toListModel
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_small : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [inst_1 : K.HasPullbacks] [P.RespectsIso] [K.Small],
  (∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y),
      P f → ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) →
    (∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y),
        (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f) →
      P.IsLocalAtTarget K
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.null_of_totalVariation_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) {i : Set α},
  s.totalVariation i = 0 → s i = 0
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.le_linearGrowthSup_iff : ∀ {u : ℕ → EReal} {a : EReal}, a ≤ LinearGrowth.linearGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in Filter.atTop, b * ↑n ≤ u n
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_ι : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.ι =
    CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.Order.SuccPred.CompleteLinearOrder
Order.IsSuccLimit.sSup_Iio : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {x : α}, Order.IsSuccLimit x → sSup (Set.Iio x) = x
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.isUnit : {α : outParam (Type u)} →
  {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → β → Option (Std.Sat.Literal α)
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- A choice of a common multiple of the denominators of a `Finset`-indexed family of fractions.  -/
IsLocalizedModule.commonDenom : {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} → Finset ι → (ι → M') → ↥S
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeights_compl : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.excenterWeights signsᶜ = s.excenterWeights signs
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIio.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α),
  Set.instFintypeIio a = Fintype.ofFinset (Finset.Iio a) ⋯
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.empty : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  AntivaryOn f g ∅
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.hom_ext_iff : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {f g : ρ.Coinvariants →ₗ[k] W},
  f = g ↔ f ∘ₗ Representation.Coinvariants.mk ρ = g ∘ₗ Representation.Coinvariants.mk ρ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.IsRankLeOne.mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R],
  Nonempty (ValuativeRel.RankLeOneStruct R) → ValuativeRel.IsRankLeOne R
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- If `C` has disjoint coproducts, any morphism out of initial is mono. Note it isn't true in
general that `C` has strict initial objects, for instance consider the category of types and
partial functions.  -/
CategoryTheory.Limits.initialMonoClass_of_coproductsDisjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.BinaryCoproductsDisjoint C],
  CategoryTheory.Limits.InitialMonoClass C
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.funext' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Add α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → (fun x => -f (x + c)) = f
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsCompleteBetween.disjoint : ∀ {V : Type u} (G : SimpleGraph V) {s t : Set V}, G.IsCompleteBetween s t → Disjoint s t
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.category : {R : Type u} → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (BialgCat R)