mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.resEquiv_inverse : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] (f : G ≃ₜ* H),
  (ContAction.resEquiv V f).inverse = ContAction.res V ↑f.symm
-- Mathlib.RingTheory.Ideal.Basic
Ideal.add_pow_mem_of_pow_mem_of_le : ∀ {α : Type u_2} {a b : α} [inst : CommSemiring α] (I : Ideal α) {m n k : ℕ},
  a ^ m ∈ I → b ^ n ∈ I → m + n ≤ k + 1 → (a + b) ^ k ∈ I
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.map_apply : ∀ {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph V) (v : V), (SimpleGraph.Iso.map f G) v = f v
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.rep_nonzero : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (v : Projectivization K V), v.rep ≠ 0
-- Init.Internal.Order.Basic
Lean.Order.instPartialOrderOption : {α : Type u_1} → Lean.Order.PartialOrder (Option α)
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.fderiv_fourierChar_neg_bilinear_right_apply : ∀ {V : Type u_1} {W : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : NormedAddCommGroup W]
  [inst_3 : NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (v : V) (w y : W),
  (fderiv ℝ (fun w => ↑(Real.fourierChar (-(L v) w))) w) y =
    -2 * ↑Real.pi * Complex.I * ↑((L v) y) * ↑(Real.fourierChar (-(L v) w))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.isoCoprod_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  (CategoryTheory.Limits.biprod.isoCoprod X Y).inv =
    CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isWeaklyRegular_append_iff' : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (rs₁ rs₂ : List R),
  RingTheory.Sequence.IsWeaklyRegular M (rs₁ ++ rs₂) ↔
    RingTheory.Sequence.IsWeaklyRegular M rs₁ ∧
      RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤)
        (List.map (⇑(Ideal.Quotient.mk (Ideal.ofList rs₁))) rs₂)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.PP.0.Lean.Meta.Grind.Arith.CommRing.toOption : Lean.Name → Thunk Lean.MessageData → Array Lean.MessageData → Option Lean.MessageData
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_C_mul_of_mul_ne_zero : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R},
  a * p.leadingCoeff ≠ 0 → (Polynomial.C a * p).degree = p.degree
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPushoutsAlongCompOfIsStableUnderCobaseChangeAlong : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) [P.IsStableUnderCobaseChangeAlong f] [P.HasPushoutsAlong f] [P.HasPushoutsAlong g],
  P.HasPushoutsAlong (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.eventually_filterAt_mem_setsAt : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (x : X), ∀ᶠ (t : Set X) in v.filterAt x, t ∈ v.setsAt x
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_map : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} (m' : M'),
  m' ∈ LieSubmodule.map f N ↔ ∃ m ∈ N, f m = m'
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sup_left : ∀ {G : Type u_1} [inst : Group G] {S T : Subgroup G} {x : G}, x ∈ S → x ∈ S ⊔ T
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddMonoid M],
  AddMonoidAlgebra.ring =
    { toSemiring := AddMonoidAlgebra.semiring, toNeg := AddMonoidAlgebra.addCommGroup.toNeg,
      toSub := AddMonoidAlgebra.addCommGroup.toSub, toZSMul := AddMonoidAlgebra.addCommGroup.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯,
      toIntCast := AddMonoidAlgebra.nonAssocRing.toAddCommGroupWithOne.toAddGroupWithOne.toIntCast, intCast_ofNat := ⋯,
      intCast_negSucc := ⋯ }
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.id_def' : ∀ {α : Type u₁} (X : α), { down := { down := ⋯ } } = CategoryTheory.CategoryStruct.id { as := X }
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.ParamKind.mk : Lean.Name → Lean.BinderInfo → Option Lean.Expr → Bool → Lean.PrettyPrinter.Delaborator.ParamKind
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesToE_map_assoc : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁')
  (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃') (f₁₂' : i₀' ⟶ i₂') (h₁₂' : CategoryTheory.CategoryStruct.comp f₁' f₂' = f₁₂')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₂ f₁₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁₂' f₃') (n₀ n₁ n₂ : ℤ),
  autoParam (β.app 0 = α.app 0) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_1 →
    autoParam (β.app 1 = α.app 2) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_3 →
      ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_5)
        (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesToE_map._auto_7) {Z : C}
        (h : X.E f₁' f₂' f₃' n₀ n₁ n₂ ⋯ ⋯ ⟶ Z),
        CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
            (CategoryTheory.CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯) h) =
          CategoryTheory.CategoryStruct.comp (X.opcyclesMap f₁₂ f₃ f₁₂' f₃' β n₁)
            (CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁' f₂' f₃' f₁₂' h₁₂' n₀ n₁ n₂ hn₁ hn₂) h)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.toPseudofunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictlyUnitaryPseudofunctor B C → CategoryTheory.Pseudofunctor B C
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (n m : ℤ) (k : R)
  (z : CochainComplex.HomComplex.Cochain F G n),
  CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The associativity diagram of an additive group object is Cartesian.

In fact, any additive monoid object whose associativity diagram is Cartesian can be made into an
additive group object (we do not prove this in this file), so we should expect that many properties
of additive group objects follow from this result.  -/
CategoryTheory.AddGrpObj.isPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.AddGrpObj A],
  CategoryTheory.IsPullback (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add A)
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.AddMonObj.add))
    CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Commute.tsum_right : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} [T2Space α] [L.NeBot] (a : α),
  (∀ (i : ι), Commute a (f i)) → Commute a (∑'[L] (i : ι), f i)
-- Lean.Parser.Command
Lean.Parser.Command.sectionHeader : Lean.Parser.Parser
-- Init.Data.UInt.Lemmas
UInt16.le_zero_iff : ∀ {a : UInt16}, a ≤ 0 ↔ a = 0
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The `LSeries` of the arithmetic function `ζ` is the same as the `LSeries` associated
to the constant sequence `1`.  -/
ArithmeticFunction.LSeries_zeta_eq : (LSeries fun n => ↑(ArithmeticFunction.zeta n)) = LSeries 1
-- Std.Http.Protocol.H1.Writer
/-- Whether the user has called `send` to provide the outgoing message head.
 -/
Std.Http.Protocol.H1.Writer.sentMessage : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Bool
-- Mathlib.Order.WellFounded
WellFounded.minimal_wellFounded_lt_min : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : WellFoundedLT α] {s : Set α} (h : s.Nonempty),
  Minimal (fun x => x ∈ s) (⋯.min s h)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.nextCoeff_map_eq : ∀ {R : Type u} {S : Type v} [inst : Ring R] [IsSimpleRing R] [inst_2 : Semiring S] [Nontrivial S] (p : Polynomial R)
  (f : R →+* S), (Polynomial.map f p).nextCoeff = f p.nextCoeff
-- Mathlib.Order.Heyting.Hom
BiheytingHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] {f g : BiheytingHom α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.dualBasis_dualBasis : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_9}
  [inst_3 : DecidableEq ι] [inst_4 : Finite ι] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate),
  B.IsSymm → ∀ (b : Module.Basis ι K V), B.dualBasis hB (B.dualBasis hB b) = b
-- Mathlib.Topology.Algebra.InfiniteSum.Order
/-- **Alias** of the forward direction of `summable_abs_iff`. -/
Summable.of_abs : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ι → α}, (Summable fun x => |f x|) → Summable f
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_iff_superpolynomialDecay_abs : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [inst : TopologicalSpace β] [inst_1 : CommRing β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Asymptotics.SuperpolynomialDecay l k f ↔ Asymptotics.SuperpolynomialDecay l (fun a => |k a|) fun a => |f a|
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type}
  [inst_1 : CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ),
  CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A K =
    K.comp
      (CategoryTheory.coyoneda.comp
        ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) C
              (Type u)).obj
          (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda A)))
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], K.truncGE e = (K.truncGE' e).extend e
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.basic : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {s : Set α}, s ∈ g → Filter.CardinalGenerateSets g s
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.mem_compl : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} {s : L.DefinableSet A α}
  {x : α → M}, x ∈ sᶜ ↔ x ∉ s
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.EMatchTheoremPtr.mk.inj : ∀ {thm thm_1 : Lean.Meta.Grind.EMatchTheorem}, { thm := thm } = { thm := thm_1 } → thm = thm_1
-- Lean.CoreM
Lean.Core.instNonemptyState : Nonempty Lean.Core.State
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.instSubsingleton : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  Subsingleton (CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  (Std.Internal.List.minKey? l).isSome = true ↔ l.isEmpty = false
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.concat : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Batteries.Data.List.Lemmas
List.finRange_eq_nil_iff : ∀ {n : ℕ}, List.finRange n = [] ↔ n = 0
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Equiv.Set.insert.congr_simp : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a : α} (H : a ∉ s),
  Equiv.Set.insert H = Equiv.Set.insert H
-- Mathlib.CategoryTheory.Limits.Creates
/-- A fully faithful functor that preserves a limit that exists also creates the limit.  -/
CategoryTheory.createsLimitOfFullyFaithfulOfPreserves : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    [CategoryTheory.Limits.HasLimit K] →
                      [CategoryTheory.Limits.PreservesLimit K F] → CategoryTheory.CreatesLimit K F
-- Mathlib.Algebra.Lie.Graded
/-- Bracket is homogeneous  -/
SetLike.GradedBracket.bracket_mem : ∀ {ι : Type u_1} {σ : Type u_2} {L : Type u_4} {inst : SetLike σ L} {inst_1 : Bracket L L} {inst_2 : Add ι} {ℒ : ι → σ}
  [self : SetLike.GradedBracket ℒ] ⦃i j : ι⦄ {gi gj : L}, gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ (i + j)
-- Init.Data.Array.Count
Array.countP_singleton : ∀ {α : Type u_1} {p : α → Bool} {a : α}, Array.countP p #[a] = if p a = true then 1 else 0
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instCoeSortType : {ι : Type t} →
  {X : ι → Type u} → [inst : (i : ι) → TopologicalSpace (X i)] → CoeSort (ContinuousGeneratedByCat X) (Type v)
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.out : ∀ {R : Type u_1} {S : Type v₃} {inst : CommSemiring R} {inst_1 : CommSemiring S} {inst_2 : Algebra R S} {R' : Type u_6}
  {S' : Type u_7} {inst_3 : CommSemiring R'} {inst_4 : CommSemiring S'} {inst_5 : Algebra R R'} {inst_6 : Algebra S S'}
  {inst_7 : Algebra R' S'} {inst_8 : Algebra R S'} {inst_9 : IsScalarTower R R' S'} {inst_10 : IsScalarTower R S S'}
  [self : Algebra.IsPushout R S R' S'], IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap
-- Mathlib.Data.List.Rotate
List.rotate_eq_self_iff_eq_replicate : ∀ {α : Type u} [hα : Nonempty α] {l : List α}, (∀ (n : ℕ), l.rotate n = l) ↔ ∃ a, l = List.replicate l.length a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_isCycle₂_iff_inv : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A] (g : G × G)
  (a : A),
  (groupHomology.IsCycle₂ fun₀ | g => a) ↔ ((fun₀ | g.2 => g.1⁻¹ • a) + fun₀ | g.1 => a) = fun₀ | g.1 * g.2 => a
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.factor_comp : ∀ {R : Type u} [inst : Ring R] {S T U : Ideal R} [inst_1 : S.IsTwoSided] [inst_2 : T.IsTwoSided] [inst_3 : U.IsTwoSided]
  (H1 : S ≤ T) (H2 : T ≤ U), (Ideal.Quotient.factor H2).comp (Ideal.Quotient.factor H1) = Ideal.Quotient.factor ⋯
-- Mathlib.FieldTheory.Galois.Basic
/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `Gal(fixedField H / K)` is isomorphic to
`Gal(L / K) ⧸ H`.  -/
IsGalois.normalAutEquivQuotient : {K : Type u_3} →
  {L : Type u_4} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [FiniteDimensional K L] →
            [IsGalois K L] →
              (H : Subgroup Gal(L/K)) → [inst_5 : H.Normal] → Gal(L/K) ⧸ H ≃* Gal(↥(IntermediateField.fixedField H)/K)
-- Mathlib.LinearAlgebra.Matrix.Cartan
Matrix.isSimplyLaced_transpose : ∀ {ι : Type u_1} (A : Matrix ι ι ℤ), A.transpose.IsSimplyLaced ↔ A.IsSimplyLaced
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensRange.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Y) (e_f : f = f_1) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.Scheme.Hom.opensRange f = AlgebraicGeometry.Scheme.Hom.opensRange f_1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyπ_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] {Z : C} (h : L.homology i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyπ i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i)
      (CategoryTheory.CategoryStruct.comp (L.homologyπ i) h)
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPtInd.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α), MeasureTheory.SimpleFunc.nearestPtInd e 0 = MeasureTheory.SimpleFunc.const α 0
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsState.mk.sizeOf_spec : ∀ (numClauses maxLit : ℕ), sizeOf { numClauses := numClauses, maxLit := maxLit } = 1 + sizeOf numClauses + sizeOf maxLit
-- Lean.Declaration
Lean.Declaration.defnDecl.injEq : ∀ (val val_1 : Lean.DefinitionVal), (Lean.Declaration.defnDecl val = Lean.Declaration.defnDecl val_1) = (val = val_1)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_submoduleMap : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] (f : M →ₛₗ[τ₁₂] M₂) (p : Submodule R M),
  (f.submoduleMap p).ker = Submodule.comap p.subtype f.ker
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.normalizedChainComplexMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C),
  SSet.normalizedChainComplexMap f R =
    CategoryTheory.CategoryStruct.comp (X.fromNormalizedChainComplex R)
      (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f R) (Y.toNormalizedChainComplex R))
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_le_ceil : ∀ {r s : ENNReal}, r ≤ s → ⌈r⌉ₑ ≤ ⌈s⌉ₑ
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E},
  fderiv 𝕜 (f ∘ ⇑iso) x = fderiv 𝕜 f (iso x) ∘SL ↑iso
-- Mathlib.Data.List.Sigma
List.kunion_nil : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {l : List (Sigma β)}, l.kunion [] = l
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves colimits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits
of shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F.unop], CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Init.Data.Iterators.Basic
/-- Termination measure to be used in recursive functions built with `WellFounded.extrinsicFix`
recursing over a finite iterator without requiring a proof of finiteness (see also `Finite`).
 -/
Std.IterM.finitelyManySteps! : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM m β → Std.IterM.TerminationMeasures.Finite α m
-- Mathlib.Topology.Instances.Rat
Rat.uniformContinuous_add : UniformContinuous fun p => p.1 + p.2
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toArray_valuesIter : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β},
  m.valuesIter.toArray = (List.map Prod.snd m.toList).toArray
-- Mathlib.Order.LiminfLimsup
Filter.mono_bliminf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α},
  (∀ (x : β), p x → u x ≤ v x) → Filter.bliminf u f p ≤ Filter.bliminf v f p
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.bottomUps : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State → Array Bool
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sumInv_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι]
  (x : AdicCompletion I (DirectSum ι fun j => M j)) (j : ι),
  ((AdicCompletion.sumInv I M) x) j = (AdicCompletion.map I (DirectSum.component R ι M j)) x
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.instFullOppositeTypeRestrictedULiftYonedaOfIsDense : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsDense], (CategoryTheory.Presheaf.restrictedULiftYoneda F).Full
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- The ring `R` is equipped with a preferred ideal.  -/
WithIdeal : (R : Type u_2) → [CommRing R] → Type u_2
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instZeroHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M₁ M₂ : PresheafOfModules R} → Zero (M₁ ⟶ M₂)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.isoMk_hom_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
  (h : A.A ≅ B.A)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom)
      CategoryTheory.Monad.Algebra.isoMk._auto_1),
  (CategoryTheory.Monad.Algebra.isoMk h w).hom.f = h.hom