mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Typecheck a `ContinuousMonoidHom` as a morphism in `ProfiniteGrp`.  -/
ProfiniteGrp.ofHom : {X Y : Type u} →
  [inst : Group X] →
    [inst_1 : TopologicalSpace X] →
      [inst_2 : IsTopologicalGroup X] →
        [inst_3 : CompactSpace X] →
          [inst_4 : TotallyDisconnectedSpace X] →
            [inst_5 : Group Y] →
              [inst_6 : TopologicalSpace Y] →
                [inst_7 : IsTopologicalGroup Y] →
                  [inst_8 : CompactSpace Y] →
                    [inst_9 : TotallyDisconnectedSpace Y] → (X →ₜ* Y) → (ProfiniteGrp.of X ⟶ ProfiniteGrp.of Y)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- One can prove `QuotientMeasureEqMeasurePreimage` by checking behavior with respect to a single
fundamental domain.  -/
MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α]
  {μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))} {s : Set α},
  MeasureTheory.IsFundamentalDomain G s ν →
    μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict s) →
      MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_coe_eq_abs_iff : ∀ (p : ℝ) {x : ℝ}, p ≠ 0 → (‖↑x‖ = |x| ↔ |x| ≤ |p| / 2)
-- Mathlib.Data.Holor
Holor.mul_zero : ∀ {ds₁ ds₂ : List ℕ} {α : Type} [inst : MulZeroClass α] (x : Holor α ds₁), x.mul 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.zsmul_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] (f : X ⟶ G) (n : ℤ)
  (g : G ⟶ H) [CategoryTheory.IsAddMonHom g],
  CategoryTheory.CategoryStruct.comp (n • f) g = n • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapAlgEquiv_residue : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing S]
  [inst_3 : CommRing T] [inst_4 : IsLocalRing T] [inst_5 : Algebra R S] [inst_6 : Algebra R T] (e : S ≃ₐ[R] T) (x : S),
  (IsLocalRing.ResidueField.mapAlgEquiv e) ((IsLocalRing.residue S) x) = (IsLocalRing.residue T) (e x)
-- Mathlib.RingTheory.RootsOfUnity.Basic
rootsOfUnity.isCyclic : ∀ (R : Type u_4) (k : ℕ) [NeZero k] [inst : CommRing R] [IsDomain R], IsCyclic ↥(rootsOfUnity k R)
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The equivalence between coarsenings of a valuation ring and its prime ideals.  -/
ValuationSubring.primeSpectrumEquiv : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → PrimeSpectrum ↥A ≃ { S // A ≤ S }
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_smul : ∀ {ι : Type u_1} {G : Type u_3} {k : Type u_5} {V : Type u_6} [inst : AddCommGroup V] [inst_1 : Ring k]
  [inst_2 : Module k V] [inst_3 : Group G] [inst_4 : DistribMulAction G V] [inst_5 : SMulCommClass G k V] (a : G)
  (b : AffineBasis ι k V) (i : ι),
  (a • b).coord i = (b.coord i).comp (↑(DistribMulAction.toLinearEquiv k V a).symm).toAffineMap
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.equivProjectivization_symm_apply_mk : ∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : DecidableEq K] (v : Fin 2 → K) (h : v ≠ 0),
  (OnePoint.equivProjectivization K).symm (Projectivization.mk K v h) =
    if v 1 = 0 then OnePoint.infty else ↑((v 1)⁻¹ * v 0)
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv.eq_3 : ∀ {α : Type u_1} [inst : DecidableEq α] (x a₁ : α), (RegularExpression.char a₁).deriv x = if a₁ = x then 1 else 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_mapWithPostcondition : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {γ : Type w} {f : β → Std.Iterators.PostconditionT n γ} [inst_1 : Monad n] [LawfulMonad n] [inst_3 : MonadLiftT m n],
  (Std.IterM.mapWithPostcondition f it).step = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let out' ← (f out).operation
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.mapWithPostcondition f it') ↑out' ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.mapWithPostcondition f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.toOpenPartialHomeomorph_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ↑φ.toOpenPartialHomeomorph = φ.prodFun
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionData.mk.sizeOf_spec : ∀ (name : Lean.Name) (expr : Lean.Expr) (projNrs : List ℕ) (isDefault isPrefix : Bool),
  sizeOf { name := name, expr := expr, projNrs := projNrs, isDefault := isDefault, isPrefix := isPrefix } =
    1 + sizeOf name + sizeOf expr + sizeOf projNrs + sizeOf isDefault + sizeOf isPrefix
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Pro-Coyoneda lemma: morphisms from colimit of coyoneda of diagram `D` to `F` is limit
of `F` evaluated at `D`. This variant is for covariant diagrams, see
`colimitCoyonedaHomIsoLimit` for a covariant version.  -/
CategoryTheory.Limits.colimitCoyonedaHomIsoLimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (D : CategoryTheory.Functor Iᵒᵖ Cᵒᵖ) →
          (F : CategoryTheory.Functor C (Type u₂)) →
            [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.coyoneda)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] →
                (CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) ≅
                  CategoryTheory.Limits.limit (D.unop.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂}))
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.mk : {L : FirstOrder.Language} →
  {T : L.Theory} →
    (Carrier : Type w) →
      [struc : L.Structure Carrier] → [is_model : Carrier ⊨ T] → [nonempty' : Nonempty Carrier] → T.ModelType
-- Mathlib.Algebra.DirectSum.Module
DirectSum.coeFnLinearMap_apply : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] (v : DirectSum ι fun i => M i), (DirectSum.coeFnLinearMap R) v = ⇑v
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_X : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Polynomial.X.degree = 1
-- Mathlib.Logic.OpClass
/-- A left-commutative operation satisfies `op a₁ (op a₂ b) = op a₂ (op a₁ b)`.  -/
LeftCommutative.left_comm : ∀ {α : Sort u} {β : Sort v} {op : α → β → β} [self : LeftCommutative op] (a₁ a₂ : α) (b : β),
  op a₁ (op a₂ b) = op a₂ (op a₁ b)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.InductionCandidate.fvarId : Lean.Meta.Try.Collector.InductionCandidate → Lean.FVarId
-- Aesop.Forward.Match.Types
Aesop.instHashableForwardRuleMatch : Hashable Aesop.ForwardRuleMatch
-- Mathlib.Analysis.CStarAlgebra.Hom
/-- A non-unital star algebra monomorphism of complex C⋆-algebras is isometric.  -/
NonUnitalStarAlgHom.nnnorm_map : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (φ : F),
  Function.Injective ⇑φ → ∀ (a : A), ‖φ a‖₊ = ‖a‖₊
-- Mathlib.Data.List.MinMax
List.maximum_concat : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α) (l : List α), (l ++ [a]).maximum = max l.maximum ↑a
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
/-- Updates the old assignment of `l` to reflect the fact that `(l, false)` is no longer part of the
formula.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNegAssignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Given an expression `e` with expected type `expectedType`, if `e` doesn't have that type,
use a cast to turn `e` into that type.  -/
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.mkCast : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Expr → Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.Small.mem₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) [inst_1 : E.Small],
  (E.restrictIndex (CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E)).presieve₀ ∈ J.coverings S
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.inv_cpow_eq_ite : ∀ (x n : ℂ), x⁻¹ ^ n = if x.arg = Real.pi then (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
/-- Given a walk that avoids a set of edges, produce a walk in the graph
with those edges deleted.  -/
SimpleGraph.Walk.toDeleteEdges : {V : Type u} →
  {G : SimpleGraph V} →
    (s : Set (Sym2 V)) → {v w : V} → (p : G.Walk v w) → (∀ e ∈ p.edges, e ∉ s) → (G.deleteEdges s).Walk v w
-- Mathlib.Topology.Path
Path.target_mem_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), y ∈ Set.range ⇑γ
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_inter`. -/
Set.diff_inter : ∀ {α : Type u_1} {s t u : Set α}, s \ (t ∩ u) = s \ t ∪ s \ u
-- Mathlib.Analysis.RCLike.Basic
instIsRCLikeNormedField : ∀ (𝕜 : Type u_3) [h : RCLike 𝕜], IsRCLikeNormedField 𝕜
-- Lean.Data.DeclarationRange
Lean.DeclarationLocation.range : Lean.DeclarationLocation → Lean.DeclarationRange
-- Batteries.Data.Fin.Coding
/-- Encode `Fin n ⊕ Fin m` into `Fin (n + m)`.  -/
Fin.encodeSum : {n m : ℕ} → Fin n ⊕ Fin m → Fin (n + m)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
  (f : Y ⟶ Y') (Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y') Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) Z)
        h)
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.ext_iff : ∀ {α : Type u} {x y : CategoryTheory.Codiscrete α}, x = y ↔ x.as = y.as
-- Mathlib.Algebra.Free
FreeMagma.traverse_pure : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : α), traverse F (pure x) = pure <$> F x
-- Init.Data.UInt.Bitwise
UInt8.neg_eq_not_add : ∀ (a : UInt8), -a = ~~~a + 1
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instNormOneClass : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], NormOneClass ℤ_[p]
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_eq_one_iff_prime : ∀ {n : ℕ}, ArithmeticFunction.cardFactors n = 1 ↔ Nat.Prime n
-- Init.Data.SInt.Lemmas
Int8.toNat_toBitVec : ∀ (x : Int8), x.toBitVec.toNat = x.toUInt8.toNat
-- Init.Prelude
/-- The "anonymous" name.  -/
Lean.Name.anonymous : Lean.Name
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.instHasFiniteColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Over X)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.instInhabited : {α : Type u₁} → [Inhabited α] → Inhabited (CategoryTheory.Discrete α)
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Expr.toSeq'.match_1.eq_1 : ∀ (motive : Lean.Grind.AC.Expr → Sort u_1) (x : Lean.Grind.AC.Var)
  (h_1 : (x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Expr.var x))
  (h_2 : (a b : Lean.Grind.AC.Expr) → motive (a.op b)),
  (match Lean.Grind.AC.Expr.var x with
    | Lean.Grind.AC.Expr.var x => h_1 x
    | a.op b => h_2 a b) =
    h_1 x
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- Notation for additive convolution with explicit bilinear map:
`(f ⋆₊[L] g) x = ∑' ab : addFiber x, L (f ab.1) (g ab.2)`.  -/
DiscreteConvolution.«term_⋆₊[_]_» : Lean.TrailingParserDescr
-- Mathlib.Order.Filter.Pointwise
Filter.vaddAssocClass'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α β] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddAssocClass α β γ], VAddAssocClass (Filter α) (Filter β) (Filter γ)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_singleton : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).reverse = SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.piCongrRight_refl : ∀ {η : Type u_16} {Ms : η → Type u_17} [inst : (j : η) → Add (Ms j)],
  (AddEquiv.piCongrRight fun j => AddEquiv.refl (Ms j)) = AddEquiv.refl ((j : η) → Ms j)
-- Mathlib.Data.List.ModifyLast
_private.Mathlib.Data.List.ModifyLast.0.List.modifyLast.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : Array α) (h_1 : (x : Array α) → motive [] x)
  (h_2 : (x : α) → (acc : Array α) → motive [x] acc)
  (h_3 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (match [], x with
    | [], x => h_1 x
    | [x], acc => h_2 x acc
    | x :: xs, acc => h_3 x xs acc) =
    h_1 x
-- Init.Data.Array.Lemmas
Array.extract_loop_of_ge : ∀ {α : Type u_1} {xs ys : Array α} {size start : ℕ}, start ≥ xs.size → Array.extract.loop xs size start ys = ys
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.mul_assoc : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Aesop.Frontend.Tactic
Aesop.Frontend.elabSimpConfig : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.Config
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.startsWith_bool_eq_false_iff_get : ∀ {p : Char → Bool} {s : String.Slice},
  s.startsWith p = false ↔ ∀ (h : s.startPos ≠ s.endPos), p (s.startPos.get h) = false
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_add : ∀ {ι : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {m : Multiset ι} {f g : ι → M},
  (Multiset.map (fun i => f i + g i) m).sum = (Multiset.map f m).sum + (Multiset.map g m).sum
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Naturality of the right unitor: commutativity of `X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y` and `X ⊗ 𝟙_ C ⟶ X ⟶ Y`
 -/
CategoryTheory.MonoidalCategory.rightUnitor_naturality : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom f
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.ofPowerSeries_X_pow : ∀ {Γ : Type u_1} [inst : Semiring Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsStrictOrderedRing Γ] {R : Type u_3}
  [inst_3 : Semiring R] (n : ℕ), (HahnSeries.ofPowerSeries Γ R) (PowerSeries.X ^ n) = (HahnSeries.single ↑n) 1
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.kernelIsoKer_hom_ker_subtype : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (ModuleCat.kernelIsoKer f).hom
      (ModuleCat.ofHom (ModuleCat.Hom.hom f).ker.subtype) =
    CategoryTheory.Limits.kernel.ι f
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Data.Int.ModEq
Int.modEq_iff_dvd : ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- The **Kruskal-Katona theorem**.

Given a set family `𝒜` consisting of `r`-sets, and `𝒞` an initial segment of the colex order of the
same size, the shadow of `𝒞` is smaller than the shadow of `𝒜`. In particular, this gives that the
minimum shadow size is achieved by initial segments of colex.  -/
Finset.kruskal_katona : ∀ {n r : ℕ} {𝒜 𝒞 : Finset (Finset (Fin n))},
  Set.Sized r ↑𝒜 → 𝒞.card ≤ 𝒜.card → Finset.Colex.IsInitSeg 𝒞 r → 𝒞.shadow.card ≤ 𝒜.shadow.card
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
Algebra.instCommRingAdjoinSingleton : {R : Type u_3} →
  {A : Type u_4} → [inst : CommRing R] → [inst_1 : Ring A] → [inst_2 : Algebra R A] → (x : A) → CommRing ↥R[x]
-- Mathlib.Algebra.Group.Basic
const_sub_involutive : ∀ {G : Type u_3} [inst : AddCommGroup G] (a : G), Function.Involutive fun x => a - x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Given a subgraph of a subgraph of `G`, construct a subgraph of `G`.  -/
SimpleGraph.Subgraph.coeSubgraph : {V : Type u} → {G : SimpleGraph V} → {G' : G.Subgraph} → G'.coe.Subgraph → G.Subgraph
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.mvarId : Lean.MVarId → Aesop.EqualUpToIds.MVarValue
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_eq_maxKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.maxKey! = t.maxKeyD default
-- Mathlib.CategoryTheory.Limits.Sifted
/-- If `C` is sifted, the canonical product comparison map for the `colim` functor
`(C ⥤ Type) ⥤ Type` is an isomorphism.  -/
CategoryTheory.IsSifted.instIsIsoObjFunctorTypeColimTensorObjProdComparison : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (X Y : CategoryTheory.Functor C (Type u))
  [CategoryTheory.IsSifted C],
  CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison CategoryTheory.Limits.colim X Y)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.homEquivOfIsRightKanExtension_symm_apply : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F),
  (F'.homEquivOfIsRightKanExtension α G).symm β = F'.liftOfIsRightKanExtension α G β
-- Batteries.Control.LawfulMonadState
/-- The namespaced `MonadStateOf.get` is equal to the `MonadState` provided `get`.  -/
monadStateOf_get_eq_get : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : MonadStateOf σ m], MonadStateOf.get = get
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.vadd_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} {G : Type u_4} [inst_1 : (i : ι) → VAdd G (R i)] [inst_2 : ∀ (i : ι), VAddMemClass (S i) G (R i)]
  (g : G) (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), (g +ᵥ x) i = g +ᵥ x i
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.weightedSumSquares.congr_simp : ∀ {S : Type u_1} (R : Type u_3) [inst : CommSemiring R] {ι : Type u_8} [inst_1 : Fintype ι] [inst_2 : Monoid S]
  [inst_3 : DistribMulAction S R] [inst_4 : SMulCommClass S R R] (w w_1 : ι → S),
  w = w_1 → QuadraticMap.weightedSumSquares R w = QuadraticMap.weightedSumSquares R w_1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.prod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N),
  s.prod t = { carrier := ↑s ×ˢ ↑t, add_mem' := ⋯ }
-- Mathlib.Data.Set.Image
Set.preimage_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {s : Set γ}, g ∘ f ⁻¹' s = f ⁻¹' g ⁻¹' s
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminalsEquivMonoOverTerminal_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C],
  (CategoryTheory.subterminalsEquivMonoOverTerminal C).unitIso =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯
-- Mathlib.FieldTheory.Normal.Basic
/-- If `E/Kᵢ/F` are towers of fields with `E/F` normal then we can lift
an algebra isomorphism `ϕ : K₁ ≃ₐ[F] K₂` to `ϕ.liftNormal E : Gal(E/F)`.  -/
AlgEquiv.liftNormal : {F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      {K₂ : Type u_4} →
        [inst_1 : Field K₁] →
          [inst_2 : Field K₂] →
            [inst_3 : Algebra F K₁] →
              [inst_4 : Algebra F K₂] →
                (K₁ ≃ₐ[F] K₂) →
                  (E : Type u_6) →
                    [inst_5 : Field E] →
                      [inst_6 : Algebra F E] →
                        [inst_7 : Algebra K₁ E] →
                          [inst_8 : Algebra K₂ E] →
                            [IsScalarTower F K₁ E] → [IsScalarTower F K₂ E] → [Normal F E] → Gal(E/F)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_subLeft : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (a : G),
  ⇑(Homeomorph.subLeft a) = fun x => a - x
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality** equality condition for nonnegative real numbers.  -/
Real.young_inequality_eq_iff_of_nonneg : ∀ {a b p q : ℝ}, 0 ≤ a → 0 ≤ b → p.HolderConjugate q → (a * b = a ^ p / p + b ^ q / q ↔ a ^ p = b ^ q)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An intersection of blocks is a block.  -/
MulAction.IsBlock.iInter : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {ι : Sort u_3} {B : ι → Set X},
  (∀ (i : ι), MulAction.IsBlock G (B i)) → MulAction.IsBlock G (⋂ i, B i)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- A cochain of degree `n : ℤ` between two cochain complexes `F` and `G` consists
of a family of morphisms `F.X p ⟶ G.X q` whenever `p + n = q`, i.e. for all
triplets in `HomComplex.Triplet n`.  -/
CochainComplex.HomComplex.Cochain : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CochainComplex C ℤ → CochainComplex C ℤ → ℤ → Type v
-- Lean.Exception
Lean.AddErrorMessageContext.add : {m : Type → Type} →
  [self : Lean.AddErrorMessageContext m] → Lean.Syntax → Lean.MessageData → m (Lean.Syntax × Lean.MessageData)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), I.support = ⊥ ↔ I = ⊤
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure.brecOn : ∀ {α : Type u_1} {S : Set (Set α)} {motive : (a : Set α) → FiniteInter.finiteInterClosure S a → Prop} {a : Set α}
  (t : FiniteInter.finiteInterClosure S a),
  (∀ (a : Set α) (t : FiniteInter.finiteInterClosure S a), FiniteInter.finiteInterClosure.below t → motive a t) →
    motive a t
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opow.eq_1 : ∀ (o₁ o₂ : ONote), o₁.opow o₂ = o₂.opowAux2 o₁.split