mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be an integral domain and `f : R[X]`. Let `s` be a finite index set.
Then a fraction of the form `f / ∏ i ∈ s, g i` evaluated in a field `K` containing `R[X]`
can be rewritten as `q + ∑ i ∈ s, r i / g i` in at most one way, where
`degree (r i) < degree (g i)`, provided that the `g i` are monic and pairwise coprime.
See `div_prod_eq_quo_add_sum_rem_div` for the existence of such a representation.  -/
Polynomial.quo_add_sum_rem_div_unique : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] {ι : Type u_3} {g : ι → Polynomial R} {s : Finset ι},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∀ {q₁ q₂ : Polynomial R} {r₁ r₂ : ι → Polynomial R},
        (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
          (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
            ↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i) → q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.ne_zero_of_degreeOf_ne_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {i : σ},
  MvPolynomial.degreeOf i p ≠ 0 → p ≠ 0
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.one_le_dual_one : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B], 1 ≤ FractionalIdeal.dual A K 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} (f : α → β → Bool),
  m₁.Equiv m₂ → (Std.HashMap.filter f m₁).Equiv (Std.HashMap.filter f m₂)
-- Mathlib.Order.OrderDual
OrderDual.ofDual_trans_toDual : ∀ {α : Type u_1}, OrderDual.ofDual.trans OrderDual.toDual = Equiv.refl αᵒᵈ
-- Mathlib.Order.CompactlyGenerated.Basic
/-- **Alias** of the reverse direction of `CompleteLattice.isSupClosedCompact_iff_wellFoundedGT`. -/
CompleteLattice.WellFoundedGT.isSupClosedCompact : ∀ (α : Type u_2) [inst : CompleteLattice α], WellFoundedGT α → CompleteLattice.IsSupClosedCompact α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_containsKey_of_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = true →
      Std.Internal.List.getValueCastD k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) fallback =
        Std.Internal.List.getValueCastD k l₁ fallback
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.comp_relation_inr : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) [inst_5 : Algebra R T]
  [inst_6 : IsScalarTower R S T] (r : σ), (Q.comp P).relation (Sum.inr r) = (MvPolynomial.rename Sum.inr) (P.relation r)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportFailure.mk.injEq : ∀ (module const : Lean.Name) (exception : Lean.Exception) (module_1 const_1 : Lean.Name) (exception_1 : Lean.Exception),
  ({ module := module, const := const, exception := exception } =
      { module := module_1, const := const_1, exception := exception_1 }) =
    (module = module_1 ∧ const = const_1 ∧ exception = exception_1)
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given a proof that two expressions `y₁ y₂ : Q($M)` are equal, construct a proof that (± `y₁`)
and (± `y₂`) are equal, where the same sign is taken in both expression.  -/
Mathlib.Tactic.FieldSimp.Sign.congr : {v : Lean.Level} →
  {M : Q(Type v)} →
    {y y' : Q(«$M»)} →
      (g : Mathlib.Tactic.FieldSimp.Sign M) →
        Q(«$y» = «$y'») →
          have a := g.expr y';
          have a_1 := g.expr y;
          Q(«$a_1» = «$a»)
-- Mathlib.Analysis.Complex.Basic
Complex.continuous_ofReal : Continuous Complex.ofReal
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.zero_apply : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] (x : P), 0 x = 0
-- Lean.Elab.MutualInductive
Lean.Elab.Command.withViewTypeRef : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadRef m] → Array Lean.Elab.Command.InductiveView → m α → m α
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [h : μ.InnerRegularCompactLTTop],
  μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) fun s => MeasurableSet s ∧ μ s ≠ ⊤
-- Aesop.Forward.State
Aesop.RuleState.mk.inj : ∀ {rule : Aesop.ForwardRule} {clusterStates : Array Aesop.ClusterState}
  {patSubstSources : Lean.PHashMap Aesop.Substitution (Lean.PHashSet Aesop.PatSubstSource)} {rule_1 : Aesop.ForwardRule}
  {clusterStates_1 : Array Aesop.ClusterState}
  {patSubstSources_1 : Lean.PHashMap Aesop.Substitution (Lean.PHashSet Aesop.PatSubstSource)},
  { rule := rule, clusterStates := clusterStates, patSubstSources := patSubstSources } =
      { rule := rule_1, clusterStates := clusterStates_1, patSubstSources := patSubstSources_1 } →
    rule = rule_1 ∧ clusterStates = clusterStates_1 ∧ patSubstSources = patSubstSources_1
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Sum of elements in a `Subring` of a `Ring` indexed by a `Finset`
is in the `Subring`.  -/
Subring.sum_mem : ∀ {R : Type u_1} [inst : Ring R] (s : Subring R) {ι : Type u_2} {t : Finset ι} {f : ι → R},
  (∀ c ∈ t, f c ∈ s) → ∑ i ∈ t, f i ∈ s
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_smul : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (q : Ideal S)
  {G : Type u_4} [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [SMulCommClass G R S] (g : G),
  (g • q).ramificationIdx R = q.ramificationIdx R
-- Mathlib.NumberTheory.ZetaValues
deriv_bernoulliFun : ∀ (k : ℕ), deriv (bernoulliFun k) = fun x => ↑k * bernoulliFun (k - 1) x
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite
on compacts and inner regular, they coincide up to a multiplicative constant.  -/
MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  [μ.InnerRegular] [μ'.InnerRegular], μ' = μ'.haarScalarFactor μ • μ
-- Mathlib.Lean.Meta.Simp
/-- Independently simplify both the left-hand side and the right-hand side
of an equality. The equality is allowed to be under binders.
Returns the simplified equality and a proof of it.  -/
Lean.Meta.simpEq : (Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result) → Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.isoOfι_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (t : CategoryTheory.Limits.Multifork I),
  t.isoOfι.hom.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_of_support_subset : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {f : Π₀ (i : ι), β i}
  {g : (i : ι) → β i → γ} {s : Finset ι}, f.support ⊆ s → (∀ i ∈ s, g i 0 = 1) → f.prod g = ∏ i ∈ s, g i (f i)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.mul.injEq : ∀ {R : Type u_1} {X : Type u_2} (a a_1 a_2 a_3 : FreeAlgebra.Pre R X), (a.mul a_1 = a_2.mul a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.load.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {a : σ → σ} {a_1 : Turing.TM2.Stmt Γ Λ σ}
  {a_2 : σ → σ} {a_3 : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2.Stmt.load a a_1 = Turing.TM2.Stmt.load a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeConstantResult.mk.inj : ∀ {snap? : Option Lean.Language.SnapshotTree} {error? : Option Lean.Exception}
  {snap?_1 : Option Lean.Language.SnapshotTree} {error?_1 : Option Lean.Exception},
  { snap? := snap?, error? := error? } = { snap? := snap?_1, error? := error?_1 } → snap? = snap?_1 ∧ error? = error?_1
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.SurjectiveOnWith.exists_pos : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : ℝ}, f.SurjectiveOnWith K C → ∃ C' > 0, f.SurjectiveOnWith K C'
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedAddHom.eq_1 : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Field β] [inst_4 : ConditionallyCompleteLinearOrder β] [inst_5 : IsStrictOrderedRing β]
  [inst_6 : Archimedean α],
  ConditionallyCompleteLinearOrderedField.inducedAddHom α β =
    { toFun := ConditionallyCompleteLinearOrderedField.inducedMap α β, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.prodUnique_symm_apply_snd : ∀ (X : Type u_1) (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Unique Y] (a : X),
  ((Homeomorph.prodUnique X Y).symm a).2 = default
-- Lean.Meta.Tactic.Grind.Types
/-- Returns initial state for registered solvers.  -/
Lean.Meta.Grind.Solvers.mkInitialStates : IO (Array Lean.Meta.Grind.SolverExtensionState)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsTwoSided.pow_add : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} [I.IsTwoSided] (m n : ℕ), I ^ (m + n) = I ^ m * I ^ n
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Nat.comap_cast_atTop : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R],
  Filter.comap Nat.cast Filter.atTop = Filter.atTop
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiable_neg_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s : (x : B) → E x},
  MDiff (T% s) → MDiff fun x => ⟨x, (-s) x⟩
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper : Lean.Meta.Grind.Arith.Cutsat.LeCnstr →
  Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.UnsatProof
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.combine.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.PairingHeapImp.Heap α → Sort u_2) →
    (x : Batteries.PairingHeapImp.Heap α) →
      ((a : α) →
          (child : Batteries.PairingHeapImp.Heap α) →
            (a_1 : α) →
              (child_1 s : Batteries.PairingHeapImp.Heap α) →
                motive
                  (Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s))) →
        ((h : Batteries.PairingHeapImp.Heap α) →
            (∀ (a : α) (child : Batteries.PairingHeapImp.Heap α) (a_1 : α)
                (child_1 s : Batteries.PairingHeapImp.Heap α),
                h = Batteries.PairingHeapImp.Heap.node a child (Batteries.PairingHeapImp.Heap.node a_1 child_1 s) →
                  False) →
              motive h) →
          motive x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f}
  (hcc : CategoryTheory.Limits.IsColimit cc) {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc)
      (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).hom h) =
    CategoryTheory.CategoryStruct.comp S.pOpcycles h
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f f_1 : F), f = f_1 → Dilation.ratio f = Dilation.ratio f_1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} {mor₁ : obj₁ ⟶ obj₂}
  {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂')
  (iso₃ : obj₃ ≅ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp iso₃.hom mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv.app j).hom₃ =
    iso₃.inv.app j
-- Mathlib.Topology.ContinuousMap.Basic
/-- The homeomorphism from the quotient of a quotient map to its codomain. This is
`Setoid.quotientKerEquivOfSurjective` as a homeomorphism.
 -/
Topology.IsQuotientMap.homeomorph : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : C(X, Y)} → Topology.IsQuotientMap ⇑f → Quotient (Setoid.ker ⇑f) ≃ₜ Y
-- Mathlib.Algebra.Ring.Opposite
RingHom.op_symm_apply_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : Rᵐᵒᵖ →+* Sᵐᵒᵖ) (a : R),
  (RingHom.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
-- Mathlib.Algebra.Order.Module.Archimedean
/-- An open ball defined by `ArchimedeanClass.submodule` of `UpperSet.Ioi c`.
For `c = ⊤`, we assign the junk value `⊥`.

This has the same carrier as `ArchimedeanClass.ballAddSubgroup`'s.  -/
FiniteArchimedeanClass.ball : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        (K : Type u_2) →
          [inst_3 : Ring K] →
            [inst_4 : LinearOrder K] →
              [IsOrderedRing K] →
                [Archimedean K] → [inst_7 : Module K M] → [PosSMulMono K M] → FiniteArchimedeanClass M → Submodule K M
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin_iff_eventuallyEq : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {x : α}, t ∈ nhdsWithin x s ↔ s =ᶠ[nhds x] s ∩ t
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.SubmonoidPresheaf.mk : {X : TopCat} →
  {F : TopCat.Presheaf CommRingCat X} →
    (obj : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ↑(F.obj U)) →
      (∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
          obj U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (obj V)) →
        F.SubmonoidPresheaf
-- Mathlib.Data.Setoid.Basic
Setoid.comap_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : Setoid γ) (g : β → γ) (f : α → β),
  Setoid.comap (g ∘ f) c = Setoid.comap f (Setoid.comap g c)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- `symm` is `true` when rewriting from right to left  -/
Mathlib.Tactic.ClickSuggestions.GrwLemma.symm : Mathlib.Tactic.ClickSuggestions.GrwLemma → Bool
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.instInhabitedStained : Inhabited Mathlib.Linter.Flexible.Stained✝
-- Mathlib.Algebra.Module.SpanRank
/-- The elements of the generators are in the submodule.  -/
Submodule.FG.generators_mem : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  p.generators ⊆ ↑p
-- Init.Data.BitVec.Lemmas
BitVec.instAssociativeHAnd : ∀ {n : ℕ}, Std.Associative fun x1 x2 => x1 &&& x2
-- Lean.Elab.Parallel
_private.Lean.Elab.Parallel.0.Std.Iterators.Types.Internal.TaskIterator.mk.injEq : ∀ {α : Type w} (tasks tasks_1 : List (Task α)), ({ tasks := tasks } = { tasks := tasks_1 }) = (tasks = tasks_1)
-- Mathlib.RingTheory.Ideal.Height
Ring.krullDimLE_of_isLocalization_maximal : ∀ {R : Type u_1} [inst : CommRing R] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2)
  [inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)]
  [inst_2 : (P : Ideal R) → [inst_2 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_3 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] {n : ℕ},
  (∀ (P : Ideal R) [inst : P.IsMaximal], Ring.KrullDimLE n (Rₚ P)) → Ring.KrullDimLE n R
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangleMorphism₁_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃),
  h.triangleMorphism₁.hom₁ = CategoryTheory.CategoryStruct.id X₁
-- Mathlib.Order.CompleteLattice.Finset
/-- Infimum of `s i`, `i : ι`, is equal to the infimum over `t : Finset ι` of infima
`⨅ i ∈ t, s i`. This version works for `ι : Sort*`. See `iInf_eq_iInf_finset` for a version
that assumes `ι : Type*` but has no `PLift`s.  -/
iInf_eq_iInf_finset' : ∀ {α : Type u_2} {ι' : Sort u_7} [inst : CompleteLattice α] (s : ι' → α), ⨅ i, s i = ⨅ t, ⨅ i ∈ t, s i.down
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.mapComp_hom_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y Z : T}
  [inst_2 : P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [inst_3 : Q.RespectsIso]
  (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g))
  (hfg : autoParam (fg = CategoryTheory.CategoryStruct.comp f g) CategoryTheory.MorphismProperty.Under.mapComp._auto_1)
  (X_1 : P.Under Q Z),
  ((CategoryTheory.MorphismProperty.Under.mapComp Q hf hg fg hfg).hom.app X_1).left =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.MorphismProperty.Under.map Q ⋯).obj X_1).toComma.1
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.printInduct : Lean.Name → List Lean.Name → ℕ → ℕ → Lean.Expr → List Lean.Name → Bool → Lean.CoreM Lean.MessageData
-- Mathlib.Order.Preorder.Chain
IsChain.preimage_embedding : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {t : Set β},
  IsChain (fun x1 x2 => x1 ≤ x2) t → ∀ (φ : α ↪o β), IsChain (fun x1 x2 => x1 ≤ x2) (⇑φ ⁻¹' t)
-- Mathlib.Algebra.Star.Module
StarAddMonoid.toStarModuleNNRat : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Module ℚ≥0 R] [inst_2 : StarAddMonoid R], StarModule ℚ≥0 R
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkStackTop.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_ofList_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.TreeMap.Raw.ofList l cmp).size ≤ l.length
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Noncomputably make a colimit cocone from the existence of unique factorizations.  -/
CategoryTheory.Limits.Cofork.IsColimit.ofExistsUnique : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {t : CategoryTheory.Limits.Cofork f g} →
          (∀ (s : CategoryTheory.Limits.Cofork f g), ∃! d, CategoryTheory.CategoryStruct.comp t.π d = s.π) →
            CategoryTheory.Limits.IsColimit t
-- Mathlib.Analysis.Meromorphic.Order
meromorphicOrderAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜], meromorphicOrderAt id 0 = 1
-- Init.Data.String.Lemmas.FindPos
String.Pos.prevn_le : ∀ {s : String} {p : s.Pos} {n : ℕ}, p.prevn n ≤ p
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.fst_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (a : B × C),
  (CategoryTheory.Bicategory.Prod.fst B C).obj a = a.1
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of `Order.Ioc_pred_left_eq_insert`. -/
Order.Ico_pred_right_eq_insert : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  b ≤ a → Set.Ioc (Order.pred b) a = insert b (Set.Ioc b a)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_toNNReal_eq : ∀ {α : Type u_1} {f : α → ENNReal}, (∀ (a : α), f a ≠ ⊤) → (∑' (a : α), f a).toNNReal = ∑' (a : α), (f a).toNNReal
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.isSuccPrelimit_type_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  Order.IsSuccPrelimit (Ordinal.type fun x1 x2 => x1 < x2) ↔ NoMaxOrder α
-- Mathlib.Data.Set.Piecewise
Set.piecewise.congr_simp : ∀ {α : Type u} {β : α → Sort v} (s s_1 : Set α),
  s = s_1 →
    ∀ (f f_1 : (i : α) → β i),
      f = f_1 →
        ∀ (g g_1 : (i : α) → β i),
          g = g_1 →
            ∀ {inst : (j : α) → Decidable (j ∈ s)} [inst_1 : (j : α) → Decidable (j ∈ s_1)] (i : α),
              s.piecewise f g i = s_1.piecewise f_1 g_1 i