mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.tprod_noncommProd : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {κ : Type u_5} (s : Finset κ) (x : κ → (i : ι) → A i)
  (hx : (↑s).Pairwise (Function.onFun Commute x)),
  (PiTensorProduct.tprod R) (s.noncommProd x hx) = s.noncommProd (fun k => (PiTensorProduct.tprod R) (x k)) ⋯
-- Mathlib.Algebra.BigOperators.Expect
Fintype.card_smul_expect : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] [inst_2 : Fintype ι] (f : ι → M),
  (Fintype.card ι • Finset.univ.expect fun i => f i) = ∑ i, f i
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The adjunction associated to a functor known to be a left adjoint.  -/
CategoryTheory.Adjunction.ofIsLeftAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (left : CategoryTheory.Functor C D) → [inst_2 : left.IsLeftAdjoint] → left ⊣ left.rightAdjoint
-- Init.Data.Nat.Lemmas
Nat.pow_le_pow_of_le : ∀ {a n m : ℕ}, 1 < a → n ≤ m → a ^ n ≤ a ^ m
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A mono factorisation coming from a strong epi-mono factorisation always has the universal
property of the image.  -/
CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (F : CategoryTheory.Limits.StrongEpiMonoFactorisation f) → CategoryTheory.Limits.IsImage F.toMonoFactorisation
-- Std.Data.ExtHashMap.Basic
/-- Updates the values of the hash map by applying the given function to all mappings.  -/
Std.ExtHashMap.map : {α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      {x : BEq α} →
        {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → (α → β → γ) → Std.ExtHashMap α β → Std.ExtHashMap α γ
-- Mathlib.Algebra.Group.End
MulAut.mul_def : ∀ (M : Type u_2) [inst : Mul M] (e₁ e₂ : MulAut M), e₁ * e₂ = MulEquiv.trans e₂ e₁
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.mul_zero_nonneg : ∀ {α : Type u_2} [inst : MulZeroClass α] {f : Filter α}, f.NeBot → 0 ≤ f * 0
-- Init.Data.Nat.Basic
Nat.lt_or_eq_of_le : ∀ {n m : ℕ}, n ≤ m → n < m ∨ n = m
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.mk.inj : ∀ {toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams} {toPartialResultParams : Lean.Lsp.PartialResultParams}
  {textDocument : Lean.Lsp.TextDocumentIdentifier} {range : Lean.Lsp.Range} {context : Lean.Lsp.CodeActionContext}
  {toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams}
  {toPartialResultParams_1 : Lean.Lsp.PartialResultParams} {textDocument_1 : Lean.Lsp.TextDocumentIdentifier}
  {range_1 : Lean.Lsp.Range} {context_1 : Lean.Lsp.CodeActionContext},
  { toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        textDocument := textDocument, range := range, context := context } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, toPartialResultParams := toPartialResultParams_1,
        textDocument := textDocument_1, range := range_1, context := context_1 } →
    toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧
      toPartialResultParams = toPartialResultParams_1 ∧
        textDocument = textDocument_1 ∧ range = range_1 ∧ context = context_1
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.smallSchroder_one : Nat.smallSchroder 1 = 1
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.Algebra.smul_def : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (a : A) (b : B) (m : M), a ⊗ₜ[R] b • m = a • b • m
-- Std.Data.Iterators.Producers.Monadic.Array
/-- The underlying state of a list iterator. Its contents are internal and should
not be used by downstream users of the library.
 -/
Std.Iterators.Types.ArrayIterator : Type w → Type w
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
/-- The set of associated primes of the product of two modules is equal to
the union of those of the two modules.  -/
associatedPrimes.prod : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (M' : Type u_3)
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'],
  associatedPrimes R (M × M') = associatedPrimes R M ∪ associatedPrimes R M'
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- The pushforward functor `PresheafOfModules R ⥤ PresheafOfModules S` induced by
a morphism of presheaves of rings `S ⟶ F.op ⋙ R`.  -/
PresheafOfModules.pushforward : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
            {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
              (S ⟶ F.op.comp R) → CategoryTheory.Functor (PresheafOfModules R) (PresheafOfModules S)
-- Mathlib.Topology.Algebra.Star
ContinuousStar.mk : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Star R], Continuous star → ContinuousStar R
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom`  -/
MonoidAlgebra.liftNCAlgHom : {R : Type u_1} →
  {A : Type u_4} →
    {B : Type u_5} →
      {M : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : Monoid M] →
                    (f : A →ₐ[R] B) →
                      (g : M →* B) → (∀ (x : A) (y : M), Commute (f x) (g y)) → MonoidAlgebra A M →ₐ[R] B
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.eval_rotateLeft : ∀ {n w : ℕ}, (Std.Tactic.BVDecide.BVUnOp.rotateLeft n).eval = fun x => x.rotateLeft n
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.instHasBinaryProductObjOfPreservesLimitDiscreteWalkingPairPair : ∀ {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 : C) [CategoryTheory.Limits.HasBinaryProduct X Y]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G],
  CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mk.congr_simp : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (toAddSubmonoid toAddSubmonoid_1 : AddSubmonoid M) (e_toAddSubmonoid : toAddSubmonoid = toAddSubmonoid_1)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier),
  { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' } = { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_iInf : ∀ {ι : Sort u_1} {M : Type u_2} [inst : AddZeroClass M] (S : ι → AddSubmonoid Mᵃᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffMulOfTopWithTopENat : ∀ {𝕜 : 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 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {a : WithTop ℕ∞} [ContMDiffMul I ⊤ G],
  ContMDiffMul I a G
-- Mathlib.CategoryTheory.Products.Basic
/-- Swapping the factors of a Cartesian product of categories twice is naturally isomorphic
to the identity functor.
 -/
CategoryTheory.Prod.symmetry : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Prod.swap C D).comp (CategoryTheory.Prod.swap D C) ≅ CategoryTheory.Functor.id (C × D)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
measurableEmbedding_sigmoid_comp_embeddingReal : ∀ (α : Type u_2) [inst : MeasurableSpace α] [inst_1 : StandardBorelSpace α],
  MeasurableEmbedding (unitInterval.sigmoid ∘ MeasureTheory.embeddingReal α)
-- Mathlib.Algebra.Group.Pi.Units
/-- **Alias** of the forward direction of `Pi.isAddUnit_iff`. -/
IsAddUnit.apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] {x : (i : ι) → M i},
  IsAddUnit x → ∀ (i : ι), IsAddUnit (x i)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.Bool.false_of_eq_true_of_eq_false : ∀ {x : Bool}, x = true → x = false → False
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- The first dart of a walk.  -/
SimpleGraph.Walk.firstDart : {V : Type u} → {G : SimpleGraph V} → {v w : V} → (p : G.Walk v w) → ¬p.Nil → G.Dart
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.binder.formatter : Lean.PrettyPrinter.Formatter
-- Init.System.IO
/-- Returns the number of _heartbeats_ that have occurred during the current thread's execution. The
heartbeat count is the number of "small" memory allocations performed in a thread.

Heartbeats used to implement timeouts that are more deterministic across different hardware.
 -/
IO.getNumHeartbeats : BaseIO ℕ
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt16.toBitVec_cond : ∀ {c : Bool} {t e : UInt16}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Init.Data.Nat.Lemmas
Nat.lt_pow_self : ∀ {n a : ℕ}, 1 < a → n < a ^ n
-- Mathlib.GroupTheory.OrderOfElement
injective_zsmul_iff_not_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, (Function.Injective fun n => n • x) ↔ ¬IsOfFinAddOrder x
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_distinguished : ∀ {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) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (X : C), (t.triangleω₁δ a b c hab hbc).obj X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.continuousOn_term : ∀ (n : ℕ), ContinuousOn (fun x => ZetaAsymptotics.term (n + 1) x) (Set.Ici 1)
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.sumInv.eq_1 : ∀ (pqr : Multiset ℕ+), ADEInequality.sumInv pqr = (Multiset.map (fun x => (↑↑x)⁻¹) pqr).sum
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rco.toList_iter : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rco α}, r.iter.toList = r.toList
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.isUnit_iff_forall_isUnit : ∀ {X : Type u_1} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : NormedRing R] [CompleteSpace R] (f : C(X, R)),
  IsUnit f ↔ ∀ (x : X), IsUnit (f x)
-- Init.Data.RArray
_private.Init.Data.RArray.0.Lean.RArray.getImpl.match_1.eq_1 : ∀ {α : Type u_1} (motive : Lean.RArray α → Sort u_2) (x : α) (h_1 : (x : α) → motive (Lean.RArray.leaf x))
  (h_2 : (p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)),
  (match Lean.RArray.leaf x with
    | Lean.RArray.leaf x => h_1 x
    | Lean.RArray.branch p l r => h_2 p l r) =
    h_1 x
-- Mathlib.Analysis.Seminorm
Seminorm.mk.inj : ∀ {𝕜 : Type u_12} {E : Type u_13} {inst : SeminormedRing 𝕜} {inst_1 : AddGroup E} {inst_2 : SMul 𝕜 E}
  {toAddGroupSeminorm : AddGroupSeminorm E}
  {smul' : ∀ (a : 𝕜) (x : E), toAddGroupSeminorm.toFun (a • x) = ‖a‖ * toAddGroupSeminorm.toFun x}
  {toAddGroupSeminorm_1 : AddGroupSeminorm E}
  {smul'_1 : ∀ (a : 𝕜) (x : E), toAddGroupSeminorm_1.toFun (a • x) = ‖a‖ * toAddGroupSeminorm_1.toFun x},
  { toAddGroupSeminorm := toAddGroupSeminorm, smul' := smul' } =
      { toAddGroupSeminorm := toAddGroupSeminorm_1, smul' := smul'_1 } →
    toAddGroupSeminorm = toAddGroupSeminorm_1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating the first of two vectors by `θ` scales their Kähler form by `cos θ - sin θ * I`.  -/
Orientation.kahler_rotation_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (θ : Real.Angle),
  (o.kahler ((o.rotation θ) x)) y = (starRingEnd ℂ) ↑θ.toCircle * (o.kahler x) y
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_7 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv x) =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f x)).inv
-- Mathlib.Algebra.Divisibility.Basic
instReflDvd_mathlib : ∀ {α : Type u_1} [inst : Monoid α], Std.Refl fun x1 x2 => x1 ∣ x2
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x + a) ⁻¹' Set.Ioo b c = Set.Ioo (b - a) (c - a)
-- Mathlib.Algebra.Order.Quantale
/-- Left- and right- residuation operators on an additive quantale are similar
to the Heyting operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ₗ z ↔ x + y ≤ z` or alternatively `x ⇨ₗ y = sSup { z | z + x ≤ y }`.  -/
AddQuantale.leftAddResiduation : {α : Type u_1} → [AddSemigroup α] → [CompleteLattice α] → α → α → α
-- Mathlib.Algebra.Order.Group.PosPart
posPart_pos_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a : α}, 0 < a⁺ ↔ 0 < a
-- Mathlib.Data.Num.Lemmas
PosNum.pred'_to_nat : ∀ (n : PosNum), ↑n.pred' = (↑n).pred
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.mem_ofAddUnits_of_isAddUnit_of_addUnit_mem : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h₁ : IsAddUnit x),
  h₁.addUnit ∈ S → x ∈ S.ofAddUnits
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.IsNested.nest : ∀ {p : DyckWord}, p.nest.IsNested
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- A locally convex space is quasi-complete if every closed and von Neumann bounded set is
complete.  -/
QuasiCompleteSpace.quasiComplete : ∀ {𝕜 : Type u_6} {E : Type u_7} {inst : Zero E} {inst_1 : UniformSpace E} {inst_2 : SeminormedRing 𝕜}
  {inst_3 : SMul 𝕜 E} [self : QuasiCompleteSpace 𝕜 E] ⦃s : Set E⦄,
  Bornology.IsVonNBounded 𝕜 s → IsClosed s → IsComplete s
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mkOfAdjoinEqTop_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
  [inst_4 : IsDomain S] [inst_5 : Module.IsTorsionFree R S] [inst_6 : IsIntegrallyClosed R] {α : S}
  (hα : IsIntegral R α) (hα₂ : R[α] = ⊤), (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root = α
-- Lean.Environment
/-- Plumbing function for `Lean.Meta.realizeValue`; see documentation there.  -/
Lean.Environment.realizeValue : {α : Type u_1} →
  [BEq α] →
    [Hashable α] →
      [TypeName α] → Lean.Environment → Lean.Name → α → (Lean.Environment → Lean.Options → BaseIO Dynamic) → IO Dynamic
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.DHashMap.Const.unitOfList l).getKey? k = none
-- Init.Data.UInt.Lemmas
UInt8.lt_one_iff : ∀ {a : UInt8}, a < 1 ↔ a = 0
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.Realize.eq_def : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (x : ℕ) (x_1 : L.BoundedFormula α x)
  (x_2 : α → M) (x_3 : Fin x → M),
  x_1.Realize x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | x, FirstOrder.Language.BoundedFormula.falsum, _v, _xs => False
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂, v, xs =>
      FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ = FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
    | x, FirstOrder.Language.BoundedFormula.rel R ts, v, xs =>
      FirstOrder.Language.Structure.RelMap R fun i => FirstOrder.Language.Term.realize (Sum.elim v xs) (ts i)
    | x, f₁.imp f₂, v, xs => f₁.Realize v xs → f₂.Realize v xs
    | x, f.all, v, xs => ∀ (x_4 : M), f.Realize v (Fin.snoc xs x_4)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (x : ↑X.toTopCat),
  (CategoryTheory.ConcreteCategory.hom e.inv.base) ((CategoryTheory.ConcreteCategory.hom e.hom.base) x) = x
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Induction principle for invertible matrices based on transvections: if a property is true for
all invertible diagonal matrices, all transvections, and is stable under product of invertible
matrices, then it is true for all invertible matrices. This is the useful way to say that
invertible matrices are generated by invertible diagonal matrices and transvections.  -/
Matrix.diagonal_transvection_induction_of_det_ne_zero : ∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (P : Matrix n n 𝕜 → Prop)
  (M : Matrix n n 𝕜),
  M.det ≠ 0 →
    (∀ (D : n → 𝕜), (Matrix.diagonal D).det ≠ 0 → P (Matrix.diagonal D)) →
      (∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix) →
        (∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)) → P M
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsRamified.comap_embedding_conjugate : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsRamified k w →
    (w.comap (algebraMap k K)).embedding = (NumberField.ComplexEmbedding.conjugate w.embedding).comp (algebraMap k K)
-- Mathlib.Combinatorics.Quiver.Path
Prefunctor.mapPath_toPath : ∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] (F : V ⥤q W) {a b : V} (f : a ⟶ b),
  F.mapPath f.toPath = (F.map f).toPath
-- Mathlib.MeasureTheory.Function.Floor
Measurable.fract : ∀ {α : Type u_1} {R : Type u_2} [inst : MeasurableSpace α] [inst_1 : Ring R] [inst_2 : LinearOrder R]
  [inst_3 : FloorRing R] [inst_4 : TopologicalSpace R] [OrderTopology R] [inst_6 : MeasurableSpace R]
  [IsStrictOrderedRing R] [BorelSpace R] {f : α → R}, Measurable f → Measurable fun x => Int.fract (f x)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlex : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Ordering
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomology_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {A : C} (f₁ f₂ : S.leftHomology ⟶ A),
  CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₁ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ f₂ →
    f₁ = f₂
-- Init.Data.List.Basic
List.Mem.below.head : ∀ {α : Type u} {a : α} {motive : (a_1 : List α) → List.Mem a a_1 → Prop} (as : List α), List.Mem.below ⋯
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- `M ↾ R` means `M.restrict R`.  -/
Matroid.«term_↾_» : Lean.TrailingParserDescr
-- Batteries.Classes.Order
Std.instLawfulOrdFin : ∀ {n : ℕ}, Std.LawfulOrd (Fin n)
-- Batteries.Util.ProofWanted
/-- Build a fresh parameter identifier name based on the last component of `n`, prefixed
according to the referenced kind (`h_` for `proof_wanted`, `d_` for `def_wanted`).  -/
_private.Batteries.Util.ProofWanted.0.freshHypName : Lean.Name → WantedRefKind✝ → Lean.Elab.Command.CommandElabM Lean.Name
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The preimage of a set `s` under a linear equiv `f` has measure
equal to `μ s` times the absolute value of the inverse of the determinant of `f`.  -/
MeasureTheory.Measure.addHaar_preimage_linearEquiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E ≃ₗ[ℝ] E) (s : Set E),
  μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ s
-- Mathlib.Algebra.Module.Torsion.Free
Module.IsTorsionFree.isSMulRegular : ∀ {R : Type u_1} {M : Type u_3} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.IsTorsionFree R M] ⦃r : R⦄, IsRegular r → IsSMulRegular M r
-- Mathlib.SetTheory.Lists
instDecidableEqLists'.decEq : {α : Type u_2} → {a : Bool} → [DecidableEq α] → (x x_1 : Lists' α a) → Decidable (x = x_1)
-- Mathlib.Logic.Pairwise
Function.injective_iff_pairwise_ne : ∀ {α : Type u_1} {ι : Type u_3} {f : ι → α}, Function.Injective f ↔ Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) f)
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.IsMulPointed.mk : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, (∀ x ∈ M, x⁻¹ ∈ M → x = 1) → M.IsMulPointed
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.support_neg : ∀ {R : Type u} (σ : Type u_1) [inst : CommRing R] {p : MvPolynomial σ R}, (-p).support = p.support
-- Mathlib.FieldTheory.Relrank
/-- **Alias** of the reverse direction of `Subfield.relfinrank_eq_one_iff`. -/
Subfield.relfinrank_eq_one_of_le : ∀ {E : Type v} [inst : Field E] {A B : Subfield E}, B ≤ A → A.relfinrank B = 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The functor defined by the over categories  -/
CategoryTheory.Over.mapFunctor : (T : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} T] → CategoryTheory.Functor T CategoryTheory.Cat
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_one : ∀ (x : ENNReal), x ^ 1 = x
-- Lean.Data.Lsp.Basic
Lean.Lsp.StaticRegistrationOptions.mk.injEq : ∀ (id? id?_1 : Option String), ({ id? := id? } = { id? := id?_1 }) = (id? = id?_1)
-- Lean.Meta.Constructions.BRecOn
/-- If `minorType` is the type of a minor premies of a recursor, such as
```
  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
```
of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
of `.below` definition; in this case
```
fun head tail tail_ih =>
  PProd (PProd (motive tail) tail_ih) PUnit
```
of type
```
α → List α → Sort (max 1 u_1) → Sort (max 1 u_1)
```
 -/
_private.Lean.Meta.Constructions.BRecOn.0.Lean.buildBelowMinorPremise : Lean.Level → Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.List.ModifyLast
List.modifyLast_append_of_right_ne_nil : ∀ {α : Type u_1} (f : α → α) (l₁ l₂ : List α), l₂ ≠ [] → List.modifyLast f (l₁ ++ l₂) = l₁ ++ List.modifyLast f l₂
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₁ = (CategoryTheory.shiftFunctor C n).map f.hom₁
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Invoke ground/symbolic evaluator from `simp`.
It uses the `seval` theorems and simprocs.
 -/
Lean.Meta.Simp.seval : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Init.Data.Bool
Bool.eq_false_imp_eq_true : ∀ {b : Bool}, b = false → b = true ↔ b = true
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
MeasurableSpace.invariants_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → α), MeasurableSpace.invariants f ≤ inst