mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Category.FinPartOrd
/-- `OrderDual` as a functor.  -/
FinPartOrd.dual : CategoryTheory.Functor FinPartOrd FinPartOrd
-- Lean.Parser.Do
/-- `return` used outside of `do` blocks creates an implicit block around it
and thus is equivalent to `pure e`, but helps with avoiding parentheses.
 -/
Lean.Parser.Term.termReturn : Lean.Parser.Parser
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instFaithfulSMulSubtypeMem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {X : Type u_4}
  [inst_3 : SMul L X] [FaithfulSMul L X] (F : IntermediateField K L), FaithfulSMul (↥F) X
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.iUnion : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → Set (Set Ω)} {s' : Set (Set Ω)}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  (∀ (n : ι), ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ) → ProbabilityTheory.Kernel.IndepSets (⋃ n, s n) s' κ μ
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.Cofibration.mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
  {inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C} [self : HomotopicalAlgebra.Cofibration f],
  HomotopicalAlgebra.cofibrations C f
-- Mathlib.NumberTheory.NumberField.Norm
/-- If `L/K` is a finite Galois extension of fields, then, for all `(x : 𝓞 L)` we have that
`x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x)`.  -/
RingOfIntegers.dvd_norm : ∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  [IsGalois K L] (x : NumberField.RingOfIntegers L),
  x ∣ (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) ((RingOfIntegers.norm K) x)
-- Mathlib.Logic.Equiv.Sum
Equiv.sigmaFiberEquiv_apply : ∀ {α : Type u_9} {β : Type u_10} (f : α → β) (x : (y : β) × { x // f x = y }), (Equiv.sigmaFiberEquiv f) x = ↑x.snd
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv.match_1.eq_1 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- If `P` is closed under colimits of shape `J`, then the inclusion creates such colimits.  -/
CategoryTheory.Limits.createsColimitsOfShapeFullSubcategoryInclusion : (J : Type w) →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (P : CategoryTheory.ObjectProperty C) →
          [P.IsClosedUnderColimitsOfShape J] →
            [CategoryTheory.Limits.HasColimitsOfShape J C] → CategoryTheory.CreatesColimitsOfShape J P.ι
-- Init.Data.UInt.Lemmas
UInt32.neg_mul_not_eq_add_mul : ∀ {a b : UInt32}, -(a * ~~~b) = a + a * b
-- Batteries.Data.Fin.Lemmas
Fin.findSomeRev?_one : ∀ {α : Type u_1} {f : Fin 1 → Option α}, Fin.findSomeRev? f = f 0
-- Mathlib.GroupTheory.Nilpotent
/-- Abelian groups are nilpotent.  -/
CommGroup.isNilpotent : ∀ {G : Type u_2} [inst : CommGroup G], Group.IsNilpotent G
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_avoid : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableEq α] {a b c : α} (P : Finpartition a),
  c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c
-- Mathlib.LinearAlgebra.Complex.Module
instStarHomClassOfSelfAdjointDecomposeOfStarOrderedRingOfStarModuleOfOrderHomClassOfLinearMapClassComplex : ∀ {F : Type u_2} {E : Type u_3} {A : Type u_4} [inst : AddCommGroup E] [inst_1 : PartialOrder E]
  [inst_2 : StarAddMonoid E] [SelfAdjointDecompose E] [inst_4 : Module ℂ E] [StarModule ℂ E] [inst_6 : NonUnitalRing A]
  [inst_7 : PartialOrder A] [inst_8 : StarRing A] [StarOrderedRing A] [inst_10 : Module ℂ A] [StarModule ℂ A]
  [inst_12 : FunLike F E A] [OrderHomClass F E A] [LinearMapClass F ℂ E A], StarHomClass F E A
-- Init.Control.ExceptCps
ExceptCpsT.instMonadExceptOf : {ε : Type u_1} → {m : Type u_1 → Type u_2} → MonadExceptOf ε (ExceptCpsT ε m)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.smul_bijective : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (m : ↥M), Function.Bijective fun s => m • s
-- Mathlib.GroupTheory.Nilpotent
Group.isNilpotent_top : ∀ {G : Type u_1} [inst : Group G], Group.IsNilpotent ↥⊤ ↔ Group.IsNilpotent G
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.IsFiltered.sequentialFunctor_final : ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsFiltered J],
  (CategoryTheory.Limits.IsFiltered.sequentialFunctor J).Final
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.instMonoid : {R : Type u_1} →
  {E : Type u_5} →
    [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → Monoid (E →ₗᵢ[R] E)
-- Lean.Meta.LetToHave
/-- This function rebuilds the expression and converts `let`s to `have`s when possible.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitLambdaLet.finalize : Array Lean.Expr → Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCochain_v_fst_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n)
  (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) {Z : C} (h_1 : K.X p₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.fst φ).f p₂) h_1) =
    CategoryTheory.CategoryStruct.comp (α.v p₁ p₂ h₁₂) h_1
-- Mathlib.Data.Real.Pointwise
Real.mul_iInf_of_nonneg : ∀ {ι : Sort u_1} {r : ℝ}, 0 ≤ r → ∀ (f : ι → ℝ), r * ⨅ i, f i = ⨅ i, r * f i
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.exists_isOpen_measure_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α), ∃ s, x ∈ s ∧ IsOpen s ∧ μ s < ⊤
-- Mathlib.Data.Finsupp.Single
Finsupp.single_of_single_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a a' : α) (b : M),
  (fun₀ | a => (fun₀ | a' => b) a) = (fun₀ | a' => fun₀ | a' => b) a
-- Init.Data.Vector.OfFn
Vector.ofFn_succ : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → α}, Vector.ofFn f = (Vector.ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.LaxBraided] [inst_7 : F'.LaxBraided] (f : F ⟶ F')
  [inst_8 : CategoryTheory.NatTrans.IsMonoidal f] (X : CategoryTheory.CommMon C),
  ((CategoryTheory.Functor.mapCommMonNatTrans f).app X).hom.hom = f.app X.X
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.getKey! k = t.getKey! k'
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.one_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : One Y] (x : X), 1 x = 1
-- Mathlib.Data.List.Cycle
/-- Given a `s : Cycle α` such that `Nodup s`, retrieve the next element after `x ∈ s`.  -/
Cycle.next : {α : Type u_1} → [DecidableEq α] → (s : Cycle α) → s.Nodup → (x : α) → x ∈ s → α
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R} (φ : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.map₂ α β).map φ).right = F.map φ.right
-- Mathlib.Order.PiLex
Pi.instDenselyOrderedColexForall : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → LT (β i)] [∀ (i : ι), DenselyOrdered (β i)],
  DenselyOrdered (Colex ((i : ι) → β i))
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- If equivalences `E : C ≌ D` and `E' : D ≌ F` are compatible with shifts, so is `E.trans E'`.
 -/
CategoryTheory.Equivalence.CommShift.instTrans : ∀ {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] (E : C ≌ D) (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : E.functor.CommShift A]
  [inst_6 : E.inverse.CommShift A] {F : Type u_4} [inst_7 : CategoryTheory.Category.{v_3, u_4} F]
  [inst_8 : CategoryTheory.HasShift F A] {E' : D ≌ F} [E.CommShift A] [inst_10 : E'.functor.CommShift A]
  [inst_11 : E'.inverse.CommShift A] [E'.CommShift A], (E.trans E').CommShift A
-- Init.Data.List.Lex
List.append_left_lt : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ l₃ : List α}, l₂ < l₃ → l₁ ++ l₂ < l₁ ++ l₃
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- Constructor for `SMulCandidate`.  -/
PresheafOfModules.Sheafify.SMulCandidate.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [CategoryTheory.Presheaf.IsLocallyInjective J α] →
              {M₀ : PresheafOfModules R₀} →
                {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                  (φ : M₀.presheaf ⟶ A.obj) →
                    [CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                      {X : Cᵒᵖ} →
                        (r : ↑(R.obj.obj X)) →
                          (m : ↑(A.obj.obj X)) →
                            (S : CategoryTheory.Sieve (Opposite.unop X)) →
                              S ∈ J (Opposite.unop X) →
                                (r₀ :
                                    CategoryTheory.Presieve.FamilyOfElements (R₀.comp (CategoryTheory.forget RingCat))
                                      S.arrows) →
                                  (m₀ :
                                      CategoryTheory.Presieve.FamilyOfElements
                                        (M₀.presheaf.comp (CategoryTheory.forget Ab)) S.arrows) →
                                    (r₀.map
                                            (CategoryTheory.Functor.whiskerRight α
                                              (CategoryTheory.forget RingCat))).IsAmalgamation
                                        r →
                                      (m₀.map
                                              (CategoryTheory.Functor.whiskerRight φ
                                                (CategoryTheory.forget Ab))).IsAmalgamation
                                          m →
                                        (a : ↑(A.obj.obj X)) →
                                          ((r₀.smul m₀).map
                                                  (CategoryTheory.Functor.whiskerRight φ
                                                    (CategoryTheory.forget Ab))).IsAmalgamation
                                              a →
                                            PresheafOfModules.Sheafify.SMulCandidate α φ r m
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_eq_zero_iff : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ → (ProbabilityTheory.evariance X μ = 0 ↔ X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
ofMul_prod : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → M),
  Additive.ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, Additive.ofMul (f i)
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_add : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] (x y : M),
  (DirectSum.decompose ℳ) (x + y) = (DirectSum.decompose ℳ) x + (DirectSum.decompose ℳ) y
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.ofDigits_mod : ∀ (b k : ℕ) (L : List ℕ), Nat.ofDigits b L % k = Nat.ofDigits (b % k) L % k
-- Mathlib.Topology.Bornology.BoundedOperation
tendsto_add_const_cobounded : ∀ {R : Type u_1} [inst : SeminormedAddCommGroup R] (x : R),
  Filter.Tendsto (fun x_1 => x_1 + x) (Bornology.cobounded R) (Bornology.cobounded R)
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.snd_comp_inl : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₂ : QuadraticMap R M₂ P),
  (QuadraticMap.Isometry.snd M₁ Q₂).comp (QuadraticMap.Isometry.inl 0 Q₂) = 0
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.injective_or_eq_zero : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSimpleModule R M] (f : M →ₗ[R] N), Function.Injective ⇑f ∨ f = 0
-- Mathlib.Algebra.Group.Basic
sub_one_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (n : ℤ), (n - 1) • a = n • a + -a
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNNNorm_diagonal : ∀ {m : Type u_3} {α : Type u_5} [inst : Fintype m] [inst_1 : SeminormedAddCommGroup α] [inst_2 : DecidableEq m]
  (v : m → α), ‖Matrix.diagonal v‖₊ = ‖v‖₊
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.inv_mem_Icc_iff : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a c d : α},
  a⁻¹ ∈ Set.Icc c d ↔ a ∈ Set.Icc d⁻¹ c⁻¹
-- Mathlib.RingTheory.WittVector.Basic
WittVector.map_coeff : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (x : WittVector p R) (n : ℕ), ((WittVector.map f) x).coeff n = f (x.coeff n)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.HashMap.Raw.unitOfList l).size = l.length
-- Std.Time.Format.Modifier
Std.Time.ZoneId.noConfusionType : Sort v✝ → Std.Time.ZoneId → Std.Time.ZoneId → Sort v✝
-- Mathlib.Combinatorics.SimpleGraph.Matching
/-- A graph `G` is alternating with respect to some other graph `G'`, if exactly every other edge in
`G` is in `G'`. Note that the degree of each vertex needs to be at most 2 for this to be
possible. This property is used to create new matchings using `symmDiff`.
The definition of `symmDiff` that makes sense is the one for `SimpleGraph`. The `symmDiff`
for `SimpleGraph.Subgraph` deriving from the lattice structure also affects the vertices included,
which we do not want in this case. This is why this property, just like `IsCycles`, is defined
for `SimpleGraph` rather than `SimpleGraph.Subgraph`.
 -/
SimpleGraph.IsAlternating : {V : Type u_1} → SimpleGraph V → SimpleGraph V → Prop
-- Mathlib.Order.Defs.Unbundled
total_of : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Total r] (a b : α), r a b ∨ r b a
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instInfClosedAddSubgroup : (G : Type u) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → Min (ClosedAddSubgroup G)
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of a scalar product is the scalar product of the trailing coefficients.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicTrailingCoeffAt (fun z => f₁ z • f₂ z) x =
        meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
-- Std.Http.Test.Helpers
/-- The terminal zero-chunk that ends a chunked body.
 -/
Std.Http.Internal.Test.chunkEnd : String
-- Mathlib.Topology.Algebra.UniformConvergence
instSubUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Sub β], instSubUniformFun = { sub := instSubUniformFun._aux_1 }
-- Plausible.Testable
Plausible.Or.printableProp : {x y : Prop} → [Plausible.PrintableProp x] → [Plausible.PrintableProp y] → Plausible.PrintableProp (x ∨ y)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- **Alias** of the forward direction of `AddSubgroup.normal_unop`. -/
AddSubgroup.Normal.of_unop : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup Gᵃᵒᵖ}, H.unop.Normal → H.Normal
-- Mathlib.CategoryTheory.Monad.Coequalizer
/-- This is the Beck cofork. It is a split coequalizer, in particular a coequalizer.  -/
CategoryTheory.Monad.beckCofork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → (X : T.Algebra) → CategoryTheory.Limits.Cofork (T.map X.a) (T.μ.app X.A)
-- Mathlib.Data.Finset.Interval
/-- Cardinality of an `Iio` of finsets.  -/
Finset.card_Iio_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, (Finset.Iio s).card = 2 ^ s.card - 1
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.mk.injEq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (support : Finset ι)
  (linearIndepOn_root : LinearIndepOn R ⇑P.root ↑support) (linearIndepOn_coroot : LinearIndepOn R ⇑P.coroot ↑support)
  (root_mem_or_neg_mem :
    ∀ (i : ι),
      P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support))
  (coroot_mem_or_neg_mem :
    ∀ (i : ι),
      P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support) ∨
        -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support))
  (support_1 : Finset ι) (linearIndepOn_root_1 : LinearIndepOn R ⇑P.root ↑support_1)
  (linearIndepOn_coroot_1 : LinearIndepOn R ⇑P.coroot ↑support_1)
  (root_mem_or_neg_mem_1 :
    ∀ (i : ι),
      P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support_1) ∨
        -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support_1))
  (coroot_mem_or_neg_mem_1 :
    ∀ (i : ι),
      P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support_1) ∨
        -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support_1)),
  ({ support := support, linearIndepOn_root := linearIndepOn_root, linearIndepOn_coroot := linearIndepOn_coroot,
        root_mem_or_neg_mem := root_mem_or_neg_mem, coroot_mem_or_neg_mem := coroot_mem_or_neg_mem } =
      { support := support_1, linearIndepOn_root := linearIndepOn_root_1,
        linearIndepOn_coroot := linearIndepOn_coroot_1, root_mem_or_neg_mem := root_mem_or_neg_mem_1,
        coroot_mem_or_neg_mem := coroot_mem_or_neg_mem_1 }) =
    (support = support_1)
-- Mathlib.RingTheory.DedekindDomain.Instances
algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul : ∀ {A : Type u_4} (B : Type u_5) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B]
  [NoZeroDivisors B] [FaithfulSMul A B] {S : Submonoid A},
  S ≤ nonZeroDivisors A → Algebra.algebraMapSubmonoid B S ≤ nonZeroDivisors B
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- `reduce` is idempotent, i.e. the maximal reduction of the maximal
reduction of a word is the maximal reduction of the word.  -/
FreeAddGroup.reduce.idem : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.reduce (FreeAddGroup.reduce L) = FreeAddGroup.reduce L
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_cons_comp_swap_zero_one : ∀ {α : Type u} {n : ℕ} (a b : α) (x : Fin n → α),
  Matrix.vecCons a (Matrix.vecCons b x) ∘ ⇑(Equiv.swap 0 1) = Matrix.vecCons b (Matrix.vecCons a x)
-- Init.Data.SInt.Bitwise
ISize.toInt8_not : ∀ (a : ISize), (~~~a).toInt8 = ~~~a.toInt8
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- `T n` is the `n`-th Chebyshev polynomial of the first kind.  -/
Polynomial.Chebyshev.T : (R : Type u_1) → [inst : CommRing R] → ℤ → Polynomial R
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k},
  (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_fun_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b},
  CurveIntegrable ω₁ γ →
    CurveIntegrable ω₂ γ → ∫ᶜ (x : E) in γ, (ω₁ x + ω₂ x) = ∫ᶜ (x : E) in γ, ω₁ x + ∫ᶜ (x : E) in γ, ω₂ x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toRealLinearMap_apply_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal) (x : α),
  (CompactlySupportedContinuousMap.toRealLinearMap f) x = ↑(f x)
-- Mathlib.Algebra.Module.Equiv.Defs
/-- For a more powerful version, see `coe_symm_mk'`.  -/
LinearEquiv.coe_symm_mk : ∀ {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] {to_fun : M → M₂} {inv_fun : M₂ → M}
  {map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y}
  {map_smul :
    ∀ (m : R) (x : M),
      { toFun := to_fun, map_add' := map_add }.toFun (m • x) =
        (RingHom.id R) m • { toFun := to_fun, map_add' := map_add }.toFun x}
  {left_inv : Function.LeftInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun}
  {right_inv : Function.RightInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun},
  ⇑{ toFun := to_fun, map_add' := map_add, map_smul' := map_smul, invFun := inv_fun, left_inv := left_inv,
          right_inv := right_inv }.symm =
    inv_fun
-- Init.Data.Vector.Lemmas
Vector.size_singleton : ∀ {α : Type u_1} {x : α}, #v[x].size = 1
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopEquiv_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.MonoidalOpposite.mopEquiv C).counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.unmopFunctor C).comp (CategoryTheory.mopFunctor C))
-- Mathlib.Logic.Equiv.Nat
/-- An equivalence between `α × α` and `α`, given that there is an equivalence between `α` and `ℕ`.
 -/
Equiv.prodEquivOfEquivNat : {α : Type u_1} → α ≃ ℕ → α × α ≃ α
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.slope_lt_derivWithin : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f S x → slope f x y < derivWithin f S x