mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.SeparableDegree
/-- **Alias** of `Irreducible.natSepDegree_eq_one_iff_of_monic'`.

---

A monic irreducible polynomial over a field `F` of exponential characteristic `q` has
separable degree one if and only if it is of the form `Polynomial.expand F (q ^ n) (X - C y)`
for some `n : ℕ` and `y : F`.  -/
Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible' : ∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q],
  f.Monic →
    Irreducible f → (f.natSepDegree = 1 ↔ ∃ n y, f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y))
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.BuiltinPropagators.mk.sizeOf_spec : ∀ (up down : Lean.Meta.Grind.PropagatorMap), sizeOf { up := up, down := down } = 1 + sizeOf up + sizeOf down
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Submodule.angle_coe : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {s : Submodule ℝ V} (x y : ↥s),
  InnerProductGeometry.angle ↑x ↑y = InnerProductGeometry.angle x y
-- Mathlib.Data.Nat.Bitwise
_private.Mathlib.Data.Nat.Bitwise.0.Nat.bitwise.eq_def : ∀ (f : Bool → Bool → Bool) (n m : ℕ),
  Nat.bitwise f n m =
    if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have r := Nat.bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffAddOfSomeENatTopOfLEInfty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {a : WithTop ℕ∞} [ContMDiffAdd I (↑⊤) G]
  [h : ENat.LEInfty a], ContMDiffAdd I a G
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Measure.ae_ne : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ] (a : α),
  ∀ᵐ (x : α) ∂μ, x ≠ a
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.shift_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n : ℤ),
      (CategoryTheory.shiftFunctor (CategoryTheory.Pretriangulated.Triangle C) n).obj T ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Combinatorics.Graph.Basic
/-- If `e` goes from `x` to `y`, it goes from `y` to `x`.  -/
Graph.isLink_symm : ∀ {α : Type u_3} {β : Type u_4} (self : Graph α β) ⦃e : β⦄, e ∈ self.edgeSet → Std.Symm (self.IsLink e)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n),
  (∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq) → z₁ = z₂
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- A group is free if it admits a free group basis. In the definition, we require the basis to
be in the same universe as `G`, although this property follows from the existence of a basis in
any universe, see `FreeGroupBasis.isFreeGroup`.  -/
IsFreeGroup : (G : Type u) → [Group G] → Prop
-- Mathlib.Topology.Constructions
continuous_quot_lift : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {r : X → X → Prop} {f : X → Y}
  (hr : ∀ (a b : X), r a b → f a = f b), Continuous f → Continuous (Quot.lift f hr)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- If `G` preserves the pullback of `(f,g)`, then the pullback comparison map for `G` at `(f,g)` is
an isomorphism.  -/
CategoryTheory.Limits.PreservesPullback.iso : {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 Z : C} →
            (f : X ⟶ Z) →
              (g : Y ⟶ Z) →
                [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] →
                  [inst_3 : CategoryTheory.Limits.HasPullback f g] →
                    [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] →
                      G.obj (CategoryTheory.Limits.pullback f g) ≅ CategoryTheory.Limits.pullback (G.map f) (G.map g)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mrefinePat(_)» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_bddBelow_range : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5}
  [Countable ι] {f : ι → δ → α}, (∀ (i : ι), Measurable (f i)) → MeasurableSet {b | BddBelow (Set.range fun i => f i b)}
-- Mathlib.CategoryTheory.Discrete.SumsProducts
_private.Mathlib.CategoryTheory.Discrete.SumsProducts.0.CategoryTheory.Discrete.productEquiv.match_5.splitter : {J : Type u_1} →
  {K : Type u_2} →
    {X Y : CategoryTheory.Discrete J × CategoryTheory.Discrete K} →
      (motive : (X ⟶ Y) → Sort u_3) → (x : X ⟶ Y) → ((f₁ : X.1 ⟶ Y.1) → (f₂ : X.2 ⟶ Y.2) → motive (f₁, f₂)) → motive x
-- Std.Data.ExtHashSet.Basic
/-- Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
collection contains multiple elements that are equal (with regard to `==`), then the last element
in the collection will be present in the returned hash set.
 -/
Std.ExtHashSet.ofArray : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Std.ExtHashSet α
-- Lean.Widget.InteractiveDiagnostic
/-- A widget instance.

`alt` is a fallback rendering of the widget
that can be shown in standard, non-interactive LSP diagnostics,
as well as when user widgets are not supported by the client.  -/
Lean.Widget.MsgEmbed.widget : Lean.Widget.WidgetInstance → Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Lean.Widget.MsgEmbed
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.mk.eq_1 : ∀ {α : Type u} (L : List (α × Bool)), FreeGroup.mk L = Quot.mk FreeGroup.Red.Step L
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_inv_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α),
  Inv.inv '' Set.Ici a = Set.Iic a⁻¹
-- Mathlib.Topology.Convenient.HomSpace
/-- Given a continuous map `f : X i → Z`, this is the map
`ContinuousMapGeneratedBy X Z T → C(X i, T)` given by the precomposition with `f`.
This is used in order to define a topology on `ContinuousMapGeneratedBy X Z T`.  -/
Topology.ContinuousMapGeneratedBy.precomp : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Z : Type v'} →
        [inst_1 : TopologicalSpace Z] →
          {T : Type v''} →
            [inst_2 : TopologicalSpace T] → {i : ι} → C(X i, Z) → Topology.ContinuousMapGeneratedBy X Z T → C(X i, T)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Cauchy–Schwarz inequality with norm  -/
norm_inner_le_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖inner 𝕜 x y‖ ≤ ‖x‖ * ‖y‖
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.le_prod_of_submultiplicative_on_pred : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : CommMonoid β] [inst_2 : Preorder β] [IsOrderedMonoid β]
  (f : α → β) (p : α → Prop),
  f 1 ≤ 1 →
    p 1 →
      (∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b) →
        (∀ (a b : α), p a → p b → p (a * b)) → ∀ (l : List α), (∀ a ∈ l, p a) → f l.prod ≤ (List.map f l).prod
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.fun.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.FunDecl pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.CodeDecl._auto_1)
  (decl_1 : Lean.Compiler.LCNF.FunDecl pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.CodeDecl._auto_1),
  (Lean.Compiler.LCNF.CodeDecl.fun decl h = Lean.Compiler.LCNF.CodeDecl.fun decl_1 h_1) = (decl = decl_1)
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- If `q ≠ 0`, the `p`-adic norm of a rational `q` is `p ^ (-padicValRat p q)`.
If `q = 0`, the `p`-adic norm of `q` is `0`.  -/
padicNorm : ℕ → ℚ → ℚ
-- Mathlib.Topology.NhdsWithin
nhdsWithin_hasBasis : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α} {a : α},
  (nhds a).HasBasis p s → ∀ (t : Set α), (nhdsWithin a t).HasBasis p fun i => s i ∩ t
-- Batteries.Data.List.Lemmas
List.idxsOf_nil : ∀ {α : Type u_1} {x : α} {s : ℕ} [inst : BEq α], List.idxsOf x [] s = []
-- Lean.MetavarContext
Lean.MVarId.isAssignable : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m Bool
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddGroup.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddGroup (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instAddGroup =
    { toAddMonoid := DirectLimit.instAddMonoid, neg := DirectLimit.map f f (fun x x_1 => -x_1) ⋯,
      sub := DirectLimit.map₂ f f f (fun x x1 x2 => x1 - x2) ⋯,
      zsmul := fun n => DirectLimit.map f f (fun x x_1 => n • x_1) ⋯, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯,
      zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mk_of_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (x : M),
  Monoid.Coprod.mk (FreeMonoid.of (Sum.inl x)) = Monoid.Coprod.inl x
-- Init.Data.SInt.Lemmas
Int8.toBitVec_neg : ∀ (x : Int8), (-x).toBitVec = -x.toBitVec
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.const.sizeOf_spec : ∀ (decl : Lean.Name), sizeOf (Aesop.ElabRuleTerm.const decl) = 1 + sizeOf decl
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal
(not necessarily unique if the ring is not commutative).  -/
isSimpleModule_iff_quot_maximal : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsSimpleModule R M ↔ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k fallback : α},
      (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Algebra.Group.Defs
/-- An abbreviation for `npowBinRec` with an additional typeclass assumption on associativity
so that we can use it in `@[csimp]` for more performant code generation.
 -/
npowBinRecAuto : {M : Type u_2} → [Semigroup M] → [One M] → ℕ → M → M
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Transport a binary bicone data via isomorphisms.  -/
CategoryTheory.Limits.BinaryBiproductData.ofIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q P' Q' : C} →
        CategoryTheory.Limits.BinaryBiproductData P Q →
          (P ≅ P') → (Q ≅ Q') → CategoryTheory.Limits.BinaryBiproductData P' Q'
-- Lean.DocString.Types
Lean.Doc.instReprDescItem : {α : Type u_1} → {β : Type u_2} → [Repr α] → [Repr β] → Repr (Lean.Doc.DescItem α β)
-- Init.Data.Rat.Lemmas
Rat.add_left_cancel : ∀ (a : ℚ) {b c : ℚ}, a + b = a + c → b = c
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_map_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {X Y : C} (f : X ⟶ Y) (y : D),
  ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction C D).map f).app y =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f y
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- The functor `w.CostructuredArrowDownwards g ⥤ w.CostructuredArrowDownwards g'` induced
by a morphism `γ` such that `R.map γ ≫ g = g'`.  -/
CategoryTheory.TwoSquare.costructuredArrowDownwardsPrecomp : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₂ X₂' : C₂} →
                            {X₃ : C₃} →
                              (g : R.obj X₂ ⟶ B.obj X₃) →
                                (g' : R.obj X₂' ⟶ B.obj X₃) →
                                  (γ : X₂' ⟶ X₂) →
                                    CategoryTheory.CategoryStruct.comp (R.map γ) g = g' →
                                      CategoryTheory.Functor (w.CostructuredArrowDownwards g)
                                        (w.CostructuredArrowDownwards g')
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The underlying additive magma.  -/
AddMagmaCat.carrier : AddMagmaCat → Type u
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
/-- The one-element family `![x]` is algebraically independent if and only if
`x` is transcendental.  -/
algebraicIndependent_iff_transcendental : ∀ {R : Type u_3} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x : A},
  AlgebraicIndependent R ![x] ↔ Transcendental R x
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.ext_iff : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  {e e' : P₁ ≃ᴬ[k] P₂}, e = e' ↔ ∀ (x : P₁), e x = e' x
-- Mathlib.Algebra.Order.GroupWithZero.Submonoid
/-- The submonoid of positive elements.  -/
Submonoid.pos : (α : Type u_1) →
  [inst : MulZeroOneClass α] →
    [inst_1 : PartialOrder α] → [PosMulStrictMono α] → [ZeroLEOneClass α] → [NeZero 1] → Submonoid α
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.map_frobenius_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) [inst_1 : ExpChar R p] {f : MvPowerSeries σ R},
  (MvPowerSeries.map (frobenius R p)) ((MvPowerSeries.expand p hp) f) = f ^ p
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.empty.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)],
  Monoid.CoprodI.Word.empty = { toList := [], ne_one := ⋯, chain_ne := ⋯ }
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst_iCycles_odd_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [inst_3 : CategoryTheory.CategoryWithHomology C] {j : ℕ},
  c.Rel (c.prev j) j →
    c.Rel j (c.next j) →
      Odd j → CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j) ψ = 0
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.snd : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {n : ℕ},
  IsMulFreimanHom n (A ×ˢ B) B Prod.snd
-- Mathlib.Algebra.Category.Grp.Basic
/-- The underlying monoid homomorphism.  -/
GrpCat.Hom.hom' : {A B : GrpCat} → A.Hom B → ↑A →* ↑B
-- Lean.Server.GoTo
Lean.Server.GoToKind.noConfusionType : Sort v✝ → Lean.Server.GoToKind → Lean.Server.GoToKind → Sort v✝
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (n : ℤ) (e : M) {L l l' : Mathlib.Tactic.FieldSimp.NF M},
  L.eval * l.eval = l'.eval → ((n, e) ::ᵣ L).eval * l.eval = ((n, e) ::ᵣ l').eval
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.seq_sub : ∀ {α β : Type u} (f : FreeAbelianGroup (α → β)) (x y : FreeAbelianGroup α), f <*> x - y = (f <*> x) - (f <*> y)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.ofSet_source : ∀ {α : Type u_1} (s : Set α), (PartialEquiv.ofSet s).source = s
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk_eq_bot : ∀ {M : Type u_1} [inst : AddZeroClass M] (toSubsemigroup : AddSubsemigroup M) (zero_mem' : 0 ∈ toSubsemigroup.carrier),
  { toAddSubsemigroup := toSubsemigroup, zero_mem' := zero_mem' } = ⊥ ↔ ↑toSubsemigroup = {0}
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_top : ∀ {V : Type u} [inst : Fintype V], ⊤.chromaticNumber = ↑(Fintype.card V)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono_on_ae₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E}
  {s : Set X} [ClosedIciTopology E],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ →
      MeasureTheory.NullMeasurableSet s μ →
        (∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x) → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopIdx.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] (i j : ι),
  RootPairing.chainTopIdx i j = if h : LinearIndependent R ![P.root i, P.root j] then Exists.choose ⋯ else j
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStar_smulRight : ∀ {E : Type u_2} {F : Type u_3} [inst : AddCommMonoid E] [inst_1 : StarAddMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : StarAddMonoid F] [inst_4 : TopologicalSpace E] [inst_5 : TopologicalSpace F] [inst_6 : ContinuousStar E]
  [inst_7 : ContinuousStar F] {S : Type u_4} [inst_8 : Semiring S] [inst_9 : StarAddMonoid S] [inst_10 : StarModule S S]
  [inst_11 : Module S E] [inst_12 : StarModule S E] [inst_13 : TopologicalSpace S] [inst_14 : ContinuousStar S]
  [inst_15 : Module S F] [inst_16 : StarModule S F] [inst_17 : ContinuousSMul S F] (f : WithConv (E →L[S] S)) (x : F),
  star (WithConv.toConv (f.ofConv.smulRight x)) = WithConv.toConv ((star f).ofConv.smulRight (star x))
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.minimalPrimes_eq_subsingleton_self : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} [I.IsPrime], I.minimalPrimes = {I}
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃_obj_map_app_app_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  {X Y : CategoryTheory.Functor C₂ D₂} (τ₂ : X ⟶ Y) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X_1 : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X_2 : C₁) (c : C₂)
  (X_3 : C₃),
  (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).map τ₂).app F₃).app X_1).app X_2).app c).app X_3 =
    ((X_1.obj (F₁.obj X_2)).map (τ₂.app c)).app (F₃.obj X_3)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sum_touchpointWeights : ∀ {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)))
  (i : Fin (n + 1)), ∑ j, s.touchpointWeights signs i j = 1
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommMonoidWithZero.toMulPosStrictMono : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α], MulPosStrictMono α
-- Init.Data.UInt.Lemmas
UInt32.zero_ne_one : 0 ≠ 1
-- Init.Data.Format.Basic
/-- As few `Format.line`s in the group as possible will be newlines.
 -/
Std.Format.FlattenBehavior.fill : Std.Format.FlattenBehavior
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_or : ∀ (a b : USize) (h : System.Platform.numBits = 64), (a ||| b).toBitVec64 h = a.toBitVec64 h ||| b.toBitVec64 h
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.mk.sizeOf_spec : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [inst_3 : SizeOf 𝕜]
  [inst_4 : SizeOf F] (toCore : PreInnerProductSpace.Core 𝕜 F) (definite : ∀ (x : F), inner 𝕜 x x = 0 → x = 0),
  sizeOf { toCore := toCore, definite := definite } = 1 + sizeOf toCore
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_ofArrows : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X} {I : Type u_1}
  (Z : I → CategoryTheory.Over X) (g : (i : I) → Z i ⟶ Y),
  (CategoryTheory.Sieve.overEquiv Y) (CategoryTheory.Sieve.ofArrows Z g) =
    CategoryTheory.Sieve.ofArrows (fun i => (Z i).left) fun i => CategoryTheory.Over.Hom.left (g i)
-- Mathlib.GroupTheory.Torsion
AddCommGroup.freeRank_congr : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] [inst_2 : AddGroup.FG G]
  [inst_3 : AddGroup.FG H] (e : G ≃+ H), AddCommGroup.freeRank G = AddCommGroup.freeRank H
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval₂_uniqueAlgEquiv : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Unique σ]
  {f : MvPolynomial σ R} {φ : R →+* S} {a : σ → S},
  Polynomial.eval₂ φ (a default) ((MvPolynomial.uniqueAlgEquiv R σ) f) = MvPolynomial.eval₂ φ a f
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.instIteratorLoop.loop : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] →
      {n : Type u → Type w} →
        [Monad n] →
          (γ : Type u) →
            (Pl : α → γ → ForInStep γ → Prop) →
              (LargeEnough : α → Prop) →
                (∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) →
                  γ →
                    (next : α) →
                      LargeEnough next → ((out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))) → n γ