mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Format.Modifier
Std.Time.Modifier.H.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.H presentation) = 1 + sizeOf presentation
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueProds.of_injective_mulHom : ∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] (f : H →ₙ* G),
  Function.Injective ⇑f → TwoUniqueProds G → TwoUniqueProds H
-- Mathlib.GroupTheory.Perm.Sign
/-- When the list `l : List α` contains all nonfixed points of the permutation `f : Perm α`,
`signAux2 l f` recursively calculates the sign of `f`.  -/
Equiv.Perm.signAux2 : {α : Type u} → [DecidableEq α] → List α → Equiv.Perm α → ℤˣ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.mem_rat_span_latticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : K),
  (NumberField.mixedEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(NumberField.mixedEmbedding.latticeBasis K))
-- Mathlib.Algebra.Star.Module
/-- Note that this lemma holds for an arbitrary `ℚ≥0`-action, rather than merely one coming from a
`DivisionSemiring`. We keep both the `nnqsmul` and `nnrat_smul` naming conventions for
discoverability. See `star_nnqsmul`.  -/
star_nnrat_smul : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : StarAddMonoid R] [inst_2 : Module ℚ≥0 R] (q : ℚ≥0) (x : R),
  star (q • x) = q • star x
-- Std.Time.Date.PlainDate
/-- Returns the first day of the week-based year for the given `year`, where weeks start on `firstDay`
and the first week must contain at least `minimalDays` days of the new year.
 -/
Std.Time.PlainDate.startOfWeekBasedYear : Std.Time.Year.Offset → Std.Time.Weekday → Std.Time.Internal.Bounded.LE 0 6 → Std.Time.PlainDate
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Eta-expanded form of `MeasureTheory.VectorMeasure.Integrable.neg` -/
MeasureTheory.VectorMeasure.Integrable.fun_neg : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {μ : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → μ.Integrable fun i => -f i
-- Mathlib.RingTheory.Spectrum.Prime.Noetherian
PrimeSpectrum.finite_setOfPred_isMin : ∀ (R : Type u) [inst : CommSemiring R] [IsNoetherianRing R], {x | IsMin x}.Finite
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  ∑'[L] (x : β), 0 = 0
-- Mathlib.NumberTheory.NumberField.Norm
/-- `Algebra.norm` as a morphism between the rings of integers.  -/
RingOfIntegers.norm : {L : Type u_1} →
  (K : Type u_2) →
    [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → NumberField.RingOfIntegers L →* NumberField.RingOfIntegers K
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y), F.stalkSpecializes h = F.stalkSpecializes h
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.head?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Min α]
  [inst_2 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.toList.head? = t.min?
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.right.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : SizeOf J] (j : J),
  sizeOf (CategoryTheory.BiconeHom.right j) = 1 + sizeOf j
-- Mathlib.CategoryTheory.Triangulated.WeakKernels
/-- If `T` is a distinguished triangle, then the kernel fork for `T.mor₂` defined in
`kernelForkOfDistTriangle` is a weak kernel fork.  -/
CategoryTheory.Pretriangulated.isWeakLimitKernelForkOfDistTriangle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (T : CategoryTheory.Pretriangulated.Triangle C) →
                (dT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) →
                  CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Pretriangulated.kernelForkOfDistTriangle T dT)
-- Init.Data.SInt.Lemmas
ISize.toInt32_ofIntLE : ∀ {n : ℤ} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt),
  (ISize.ofIntLE n h₁ h₂).toInt32 = Int32.ofInt n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.lt_int_module : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LT α] (ctx : Lean.Grind.CommRing.Context α)
  (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx p < 0 → Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p < 0
-- Std.Net.Addr
Std.Net.IPAddr.v6.inj : ∀ {addr addr_1 : Std.Net.IPv6Addr}, Std.Net.IPAddr.v6 addr = Std.Net.IPAddr.v6 addr_1 → addr = addr_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α}, k ∈ Std.ExtTreeMap.filterMap f t → k ∈ t
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.extendScalars.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E E_1 : IntermediateField K L} (e_E : E = E_1) (h : F ≤ E),
  IntermediateField.extendScalars h = IntermediateField.extendScalars ⋯
-- Init.Data.SInt.Lemmas
UInt8.toInt8_mul : ∀ (a b : UInt8), (a * b).toInt8 = a.toInt8 * b.toInt8
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_abs_base : ∀ (b x : ℝ), Real.logb |b| x = Real.logb b x
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_setWidth : ∀ {n : ℕ} (i : ℕ) (x : BitVec n), (BitVec.setWidth i x).toNat = x.toNat % 2 ^ i
-- Mathlib.Algebra.Star.Basic
star_zpow : ∀ {R : Type u} [inst : Group R] [inst_1 : StarMul R] (x : R) (z : ℤ), star (x ^ z) = star x ^ z
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] {Y' : C} (f : X ⟶ Y') (s : Y ⟶ Y') (hs : W s),
  sizeOf { Y' := Y', f := f, s := s, hs := hs } = 1 + sizeOf Y' + sizeOf f + sizeOf s + sizeOf hs
-- Mathlib.Tactic.CategoryTheory.Elementwise
/-- The `elementwise` attribute can be added to a lemma proving an equation of morphisms, and it
creates a new lemma for a `ConcreteCategory` giving an equation with those morphisms applied
to some value.

Syntax examples:
- `@[elementwise]`
- `@[elementwise nosimp]` to not use `simp` on both sides of the generated lemma
- `@[elementwise (attr := simp)]` to apply the `simp` attribute to both the generated lemma and
  the original lemma.

Example application of `elementwise`:

```lean
@[elementwise]
lemma some_lemma {C : Type*} [Category* C]
    {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) : f ≫ g = h := ...
```

produces

```lean
lemma some_lemma_apply {C : Type*} [Category* C]
    {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...)
    {CC : ...} {FC : ...} [...] [ConcreteCategory C FC] (x : ToType X) : g (f x) = h x := ...
```

Here `f`, `g`, and `h` are being coerced to functions via
`CategoryTheory.ConcreteCategory.instCoeFunHomForallToType`.
Further, we simplify the type using `CategoryTheory.coe_id : ((𝟙 X) : X → X) x = x` and
`CategoryTheory.coe_comp : (f ≫ g) x = g (f x)`,
replacing morphism composition with function composition.

The `[ConcreteCategory C FC]` and related arguments will be omitted if it is possible to synthesize
an instance.

The name of the produced lemma can be specified with `@[elementwise other_lemma_name]`.
If `simp` is added first, the generated lemma will also have the `simp` attribute.
 -/
Mathlib.Tactic.Elementwise.elementwise : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.tail_support_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  (p.append p').support.tail = p.support.tail ++ p'.support.tail
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (s : CategoryTheory.Limits.Cocone F)
  {U V : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ} (i : U ⟶ V),
  CategoryTheory.CategoryStruct.comp (s.pt.presheaf.map i)
      (AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s V) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s U)
      (((TopCat.Presheaf.pushforward C
                (CategoryTheory.Limits.colimit.desc (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
                  ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).obj
            (AlgebraicGeometry.PresheafedSpace.colimitCocone F).pt.presheaf).map
        i)
-- Mathlib.SetTheory.ZFC.Class
Class.sUnion_apply : ∀ {x : Class.{u_1}} {y : ZFSet.{u_1}}, x.sUnion y ↔ ∃ z, x z ∧ y ∈ z
-- Mathlib.Computability.StateTransition
StateTransition.reaches₁_fwd : ∀ {σ : Type u_1} {f : σ → Option σ} {a b c : σ},
  StateTransition.Reaches₁ f a c → b ∈ f a → StateTransition.Reaches f b c
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply : ∀ (G H : AddCommGrpCat) (x : ↑G × ↑H),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.snd)
      ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) =
    x.2
-- Init.Data.Nat.Basic
/-- Alias for `Nat.ne_iff_lt_or_gt`.  -/
Nat.lt_or_gt : ∀ {a b : ℕ}, a ≠ b ↔ a < b ∨ b < a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_maxKey_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} (hc : k ∈ t), (compare k (t.maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.cochainComplex_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X) (n₁ n₂ : ℤ) (k₁ k₂ : ℕ)
  (h₁ : autoParam (-↑k₁ = n₁) CategoryTheory.ProjectiveResolution.cochainComplex_d._auto_1)
  (h₂ : autoParam (-↑k₂ = n₂) CategoryTheory.ProjectiveResolution.cochainComplex_d._auto_3),
  R.cochainComplex.d n₁ n₂ =
    CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n₁ k₁ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (R.complex.d k₁ k₂) (R.cochainComplexXIso n₂ k₂ ⋯).inv)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.range_eq_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {H : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  Set.range ↑I.toPartialEquiv = I.target
-- Lean.Elab.Tactic.RCases
/-- This function is used for producing rcases patterns based on a case tree. This is like
`tuple₁Core` but it produces a pattern instead of a tuple pattern list, converting `[n]` to `n`
instead of `⟨n⟩` and `[]` to `_`, and otherwise just converting `[a, b, c]` to `⟨a, b, c⟩`.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.RCasesPatt.tuple₁ : List Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.Algebra.Group.Action.Defs
IsScalarTower.left : ∀ (M : Type u_1) {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α], IsScalarTower M M α
-- Mathlib.Dynamics.OmegaLimit
nonempty_omegaLimit : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  [CompactSpace β] [f.NeBot], s.Nonempty → (omegaLimit f ϕ s).Nonempty
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.eulerCharSignsUpInt : (ComplexShape.up ℤ).EulerCharSigns
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAdd : {R : Type u_3} → {A : Type u_4} → [Add R] → [Add A] → Add (Unitization R A)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.domRestrict_ker_self : ∀ {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₂}
  (f : M →ₛₗ[τ₁₂] M₂), f.domRestrict f.ker = 0
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instPartialOrder : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → PartialOrder (CategoryTheory.Precoverage C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_negY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).negY (⇑f ∘ P) = f ((W'.baseChange A).negY P)
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.ext_iff_smul : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] {A B : Matrix n n R},
  A = B ↔ ∀ (v : n → R), A • v = B • v
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.natCoe_mul : ∀ {R : Type u_1} [inst : Semiring R] {f g : ArithmeticFunction ℕ}, ↑(f * g) = ↑f * ↑g
-- Mathlib.Order.Ideal
Order.Ideal.biSup_mem_iff : ∀ {P : Type u_1} [inst : CompleteLattice P] {I : Order.Ideal P} {α : Type u_2} {f : α → P} {s : Set α},
  s.Finite → (⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I)
-- Mathlib.Tactic.ComputeDegree
/-- `getCongrLemma (lhs_name, rel_name, Mvars?)` returns the name of a lemma that preprocesses
one of the seven targets
*  `natDegree f ≤ d`;
*  `natDegree f < d`;
*  `natDegree f = d`;
*  `degree f ≤ d`;
*  `degree f < d`;
*  `degree f = d`.
*  `coeff f d = r`.

The end goals are of the form
* `natDegree f ≤ ?_`, `degree f ≤ ?_`, `coeff f ?_ = ?_`, or `?_ < d` with fresh metavariables;
* `coeff f m ≠ s` with `m, s` not necessarily metavariables;
* several equalities/inequalities between expressions and assignments for metavariables.

`getCongrLemma` gets called at the very beginning of `compute_degree` and whenever an intermediate
goal does not have the right metavariables.
Note that the side-goals of the congruence lemma are neither of the form `natDegree f = d` nor
of the form `degree f = d`.

`getCongrLemma` admits an optional "debug" flag: `getCongrLemma data true` prints the name of
the congruence lemma that it returns.
 -/
Mathlib.Tactic.ComputeDegree.getCongrLemma : Lean.Name × Lean.Name × List Bool → optParam Bool false → Lean.Name
-- Mathlib.Data.Bool.Basic
Bool.or_le : ∀ {x y z : Bool}, x ≤ z → y ≤ z → (x || y) ≤ z
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.descTruncGT_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ [t.IsGE Y n₁], ∃ f', f = CategoryTheory.CategoryStruct.comp ((t.truncGTπ n₀).app X) f'
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.comp_assoc : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B]
  [inst_6 : Star B] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] [inst_10 : Semiring D]
  [inst_11 : Algebra R D] [inst_12 : Star D] (f : C →⋆ₐ[R] D) (g : B →⋆ₐ[R] C) (h : A →⋆ₐ[R] B),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.ofNatCode.eq_2 : Nat.Partrec.Code.ofNatCode 1 = Nat.Partrec.Code.succ
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSets_singleton_iff : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s t : Set Ω} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.IndepSets {s} {t} κ μ ↔ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.fun_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Neg β] [ContinuousNeg β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun i => -f i) μ
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
PowerSeries.WithPiTopology.tprod_one_sub_X_pow : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] [T2Space R],
  ∏' (n : ℕ), (1 - PowerSeries.X ^ (n + 1)) = PowerSeries.pentagonalSeries R
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Turn a subfield of `L` containing the image of `K` into an intermediate field.  -/
Subfield.toIntermediateField : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → (S : Subfield L) → (∀ (x : K), (algebraMap K L) x ∈ S) → IntermediateField K L
-- Mathlib.Algebra.CharP.Invertible
CharP.intCast_mul_natCast_gcdA_eq_gcd : ∀ {R : Type u_1} [inst : Ring R] {p : ℕ} [CharP R p] (n : ℕ), ↑n * ↑(n.gcdA p) = ↑(n.gcd p)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
PresheafOfModules.injective_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Mono f] (X : Cᵒᵖ),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.tag_injective : ∀ {ι : Type u_1} (n : ℕ) [NeZero n], Function.Injective fun ν => BoxIntegral.unitPartition.tag n ν
-- Init.Data.Repr
instReprSourceInfo.repr : Lean.SourceInfo → ℕ → Std.Format
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_addLeftHom_apply : ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} (c : Multiplicative G),
  ⇑(AddConstMap.addLeftHom c) = Multiplicative.toAdd c +ᵥ id
-- Mathlib.Topology.Constructions
/-- The identity equivalence between `X` and `CofiniteTopology X`.  -/
CofiniteTopology.of : {X : Type u} → X ≃ CofiniteTopology X
-- Mathlib.Tactic.Qify
Mathlib.Tactic.Qify.intCast_eq : ∀ (a b : ℤ), a = b ↔ ↑a = ↑b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_eq_get_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {a : α} {h' : a ∈ t}, t.getKey a h' = (t.getKey? a).get ⋯
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.mul_one_sub_self : ∀ {R : Type u_1} [inst : NonAssocRing R] {a : R}, IsIdempotentElem a → a * (1 - a) = 0
-- Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
CategoryTheory.ObjectProperty.hasCardinalLT_subtype_ofObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (X : ι → C) {κ : Cardinal.{w}},
  HasCardinalLT ι κ → (CategoryTheory.ObjectProperty.ofObj X).HasCardinalLT κ
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.one.inj : ∀ {ref : Lean.Syntax} {a : Lean.Name} {ref_1 : Lean.Syntax} {a_1 : Lean.Name},
  Lean.Elab.Tactic.RCases.RCasesPatt.one ref a = Lean.Elab.Tactic.RCases.RCasesPatt.one ref_1 a_1 →
    ref = ref_1 ∧ a = a_1
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.pre_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat),
  CategoryTheory.Grothendieck.pre F (CategoryTheory.Functor.id C) =
    CategoryTheory.Functor.id (CategoryTheory.Grothendieck ((CategoryTheory.Functor.id C).comp F))
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Given a point `p₀` in a set of points, that set is collinear if and
only if the points can all be expressed as multiples of the same
vector, added to `p₀`.  -/
collinear_iff_of_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p₀ : P}, p₀ ∈ s → (Collinear k s ↔ ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivInverse_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) {J : Type w}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) {X Y : CategoryTheory.Limits.Cone F}
  (f : X ⟶ Y),
  ((CategoryTheory.Over.ConstructProducts.conesEquivInverse B F).map f).hom = CategoryTheory.Over.Hom.left f.hom
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.hasAffineProperty : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsIntegralHom fun X x f x_1 =>
  AlgebraicGeometry.IsAffine X ∧ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ⊤)).IsIntegral
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_le_of_le_one_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosMono α],
  0 ≤ b → a ≤ 1 → a * b ≤ b
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiable.coordChangeL : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [inst_18 : MemTrivializationAtlas e]
  [inst_19 : MemTrivializationAtlas e'] [inst_20 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {f : M → B},
  MDiff f →
    (∀ (x : M), f x ∈ e.baseSet) →
      (∀ (x : M), f x ∈ e'.baseSet) → MDiff fun y => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mapₙₐ_apply : ∀ {n : Type u_2} {R : Type u_3} {A : Type u_5} {B : Type u_6} [inst : Fintype n] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : Star A] [inst_5 : NonUnitalNonAssocSemiring B]
  [inst_6 : Module R B] [inst_7 : Star B] (f : A →⋆ₙₐ[R] B) (M : CStarMatrix n n A),
  (CStarMatrix.mapₙₐ f) M = (CStarMatrix.mapₗ ↑f) M
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to
that of `E`.  -/
Submodule.finrank_add_finrank_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] (K : Submodule 𝕜 E), Module.finrank 𝕜 ↥K + Module.finrank 𝕜 ↥Kᗮ = Module.finrank 𝕜 E