mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.map_apply_ιMulti_family : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {I : Type u_4} [inst_5 : LinearOrder I] (v : I → M) (f : M →ₗ[R] N)
  (s : ↑(Set.powersetCard I n)),
  (exteriorPower.map n f) (exteriorPower.ιMulti_family R n v s) = exteriorPower.ιMulti_family R n (⇑f ∘ v) s
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- At the base point `u.1`, the implicit function evaluates to `u.2`.  -/
ContDiffAt.implicitFunction_apply_self : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible), cdf.implicitFunction pn if₂ u.1 = u.2
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.instCategoryStructHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      {X Y : CategoryTheory.CatEnrichedOrdinary C} → CategoryTheory.CategoryStruct.{v', v} (X ⟶ Y)
-- Mathlib.RingTheory.Ideal.Maps
RingHom.liftOfRightInverse.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (f_inv f_inv_1 : B → A) (e_f_inv : f_inv = f_inv_1) (hf : Function.RightInverse f_inv ⇑f),
  f.liftOfRightInverse f_inv hf = f.liftOfRightInverse f_inv_1 ⋯
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.mapMulHom_coe : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] (f : α →ₙ* β) (a : α), (WithOne.mapMulHom f) ↑a = ↑(f a)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.hom_heq_of_cons_eq_cons : ∀ {V : Type u} [inst : Quiver V] {a b c d : V} {p : Quiver.Path a b} {p' : Quiver.Path a c} {e : b ⟶ d} {e' : c ⟶ d},
  p.cons e = p'.cons e' → e ≍ e'
-- Lean.InternalExceptionId
Lean.InternalExceptionId.mk : ℕ → Lean.InternalExceptionId
-- Mathlib.Order.RelClasses
/-- Set notation form of `Ne.lt_of_le` -/
Ne.ssubset_of_subset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ≠ b → a ⊆ b → a ⊂ b
-- Init.Data.String.Subslice
String.Slice.Subslice.startInclusive_toSlice : ∀ {s : String.Slice} {sl : s.Subslice}, sl.toSlice.startInclusive = sl.startInclusive.str
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Restriction of a measure to a subset is monotone both in set and in measure.  -/
MeasureTheory.Measure.restrict_mono' : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄ ⦃μ ν : MeasureTheory.Measure α⦄,
  s ≤ᵐ[μ] s' → μ ≤ ν → μ.restrict s ≤ ν.restrict s'
-- Init.Data.List.Basic
List.Lex.below.rel : ∀ {α : Type u} {r : α → α → Prop} {motive : (as bs : List α) → List.Lex r as bs → Prop} {a₁ : α} {l₁ : List α} {a₂ : α}
  {l₂ : List α} (h : r a₁ a₂), List.Lex.below ⋯
-- Mathlib.Data.Analysis.Topology
Ctop.inter_sub : ∀ {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (a b : σ) (x : α) (h : x ∈ self.f a ∩ self.f b),
  self.f (self.inter a b x h) ⊆ self.f a ∩ self.f b
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snocCases.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {motive : ((i : Fin n.succ) → α i) → Sort u_2}
  (snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (Fin.last n)) → motive (Fin.snoc xs x))
  (x : (i : Fin n.succ) → α i), Fin.snocCases snoc x = cast ⋯ (snoc (Fin.init x) (x (Fin.last n)))
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFiniteAt.of_isOpen_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsArtinianRing R]
  (p : PrimeSpectrum S) [Algebra.FiniteType R S], IsOpen {p} → Algebra.QuasiFiniteAt R p.asIdeal
-- Mathlib.RingTheory.Polynomial.Wronskian
/-- `natDegree` version of the above theorem.
Note this would be false with just `(ha : a ≠ 0)` and `(hb : b ≠ 0)`,
since when `a = b = 1` we have `(wronskian a b).natDegree = a.natDegree = b.natDegree = 0`.
 -/
Polynomial.natDegree_wronskian_lt_add : ∀ {R : Type u_1} [inst : CommRing R] {a b : Polynomial R},
  a.wronskian b ≠ 0 → (a.wronskian b).natDegree < a.natDegree + b.natDegree
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Week.Offset` from a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.subWeeks : Std.Time.PlainDateTime → Std.Time.Week.Offset → Std.Time.PlainDateTime
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.comap_top : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F), NonUnitalSubsemiring.comap f ⊤ = ⊤
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
List.iSup_mem_map_of_ne_nil : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {l : List ι} (f : ι → α),
  l ≠ [] → ⨆ x ∈ l, f x ∈ List.map f l
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
sSup_iUnion_Iic : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α),
  sSup (⋃ i, Set.Iic (f i)) = ⨆ i, f i
-- Mathlib.Order.GaloisConnection.Defs
/-- Make a `GaloisInsertion l u` from a `GaloisConnection l u` such that `∀ b, b ≤ l (u b)`  -/
GaloisConnection.toGaloisInsertion : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {l : α → β} → {u : β → α} → GaloisConnection l u → (∀ (b : β), b ≤ l (u b)) → GaloisInsertion l u
-- Mathlib.Tactic.Zify
/-- The `Simp.Context` generated by `zify`.  -/
Mathlib.Tactic.Zify.mkZifyContext : Option (Lean.Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",") →
  Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.MkSimpContextResult
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α}, (cmp t.maxKey! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- The cocone glued from the `colim Dᵢ`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰 →
                      [∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                            CategoryTheory.Limits.PreservesColimitsOfShape J
                              (CategoryTheory.MorphismProperty.Over.pullback P ⊤
                                (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))] →
                        [Quiver.IsThin 𝒰.I₀] →
                          [Small.{u, u_2} 𝒰.I₀] →
                            [AlgebraicGeometry.IsZariskiLocalAtTarget P] → CategoryTheory.Limits.Cocone D
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.isDefault : Lean.IR.Alt → Bool
-- Mathlib.Data.NNReal.Basic
NNReal.iSup_mul_iSup_le : ∀ {ι : Sort u_3} {a : NNReal} {g h : ι → NNReal}, (∀ (i j : ι), g i * h j ≤ a) → iSup g * iSup h ≤ a
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.upper.eq_1 : ∀ (α : Type u_1) [inst : Preorder α], Topology.upper α = TopologicalSpace.generateFrom {s | ∃ a, (Set.Iic a)ᶜ = s}
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformlyOnFilter.sub` -/
TendstoUniformlyOnFilter.fun_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformlyOnFilter f g l l' →
    TendstoUniformlyOnFilter f' g' l l' →
      TendstoUniformlyOnFilter (fun i i_1 => f i i_1 - f' i i_1) (fun i => g i - g' i) l l'
-- Mathlib.Data.List.Chain
List.isChain_reverse : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l.reverse ↔ List.IsChain (fun a b => R b a) l
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.invtRootSubmodule.eq_top_iff : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {K : Type u_5}
  [inst_2 : Field K] [inst_3 : Module K M] [inst_4 : Module K N] {P : RootPairing ι K M N} [P.IsRootSystem]
  (q : ↥P.invtRootSubmodule), q = ⊤ ↔ Set.range ⇑P.root ⊆ ↑↑q
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.rotateL : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      ¬l.size + r.size ≤ 1 →
        Ordnode.delta * l.size < r.size →
          2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3 → Ordnode.Valid' o₁ (l.rotateL x r) o₂
-- Mathlib.Algebra.Tropical.Basic
Tropical.tropRec.eq_1 : ∀ {R : Type u} {F : Tropical R → Sort v} (h : (X : R) → F (Tropical.trop X)) (X : Tropical R),
  Tropical.tropRec h X = h (Tropical.untrop X)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.sup_eq_prod_inf_factors : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I J : Ideal T},
  I ≠ ⊥ →
    J ≠ ⊥ → I ⊔ J = (UniqueFactorizationMonoid.normalizedFactors I ∩ UniqueFactorizationMonoid.normalizedFactors J).prod
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.ccos : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ},
  AEMeasurable f μ → AEMeasurable (fun x => Complex.cos (f x)) μ
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_inv : ∀ {Γ₀ : Type u_4} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_7} [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (x : R), v x⁻¹ = (v x)⁻¹
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Destructor for M-type of `P`  -/
MvPFunctor.M.dest' : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} →
      {x : P.last.M} →
        {a : P.A} →
          {f : P.last.B a → P.last.M} → x.dest = ⟨a, f⟩ → TypeVec.Arrow (MvPFunctor.M.Path P x) α → ↑P (α ::: P.M α)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opUnopIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), F.opUnopIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.sub_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄), (h.sub h').h₀ = h.h₀ - h'.h₀
-- Mathlib.Analysis.Calculus.Deriv.Inv
hasDerivWithinAt_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜},
  x ≠ 0 → ∀ (s : Set 𝕜), HasDerivWithinAt (fun x => x⁻¹) (-(x ^ 2)⁻¹) s x
-- Init.Grind.Lemmas
Lean.Grind.and_eq_of_eq_false_left : ∀ {a b : Prop}, a = False → (a ∧ b) = False
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.isZero_opcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ),
  CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f)) →
    CategoryTheory.Limits.IsZero (X.opcycles f g n)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m '' Set.Icc i j = Set.Icc (Fin.natAdd m i) (Fin.natAdd m j)
-- Init.Data.List.Impl
List.findRev?_eq_find?_reverse : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, List.findRev? p l = List.find? p l.reverse
-- Init.Control.Lawful.Instances
ExceptT.run_bind_lift : ∀ {m : Type u_1 → Type u_2} {α ε β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β),
  (ExceptT.lift x >>= f).run = do
    let a ← x
    (f a).run
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubringClass.subtype_apply : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : SetLike S R] [hSR : NonUnitalSubringClass S R]
  {s : S} (x : ↥s), (NonUnitalSubringClass.subtype s) x = ↑x
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Icc_add_Icc_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α] (a b c d : α),
  Set.Icc a b + Set.Icc c d ⊆ Set.Icc (a + c) (b + d)
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.coe_div : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a b : { x // 0 ≤ x }),
  ↑(a / b) = ↑a / ↑b
-- Mathlib.Order.RelIso.Basic
RelIso.mk.inj : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} {toEquiv : α ≃ β}
  {map_rel_iff' : ∀ {a b : α}, s (toEquiv a) (toEquiv b) ↔ r a b} {toEquiv_1 : α ≃ β}
  {map_rel_iff'_1 : ∀ {a b : α}, s (toEquiv_1 a) (toEquiv_1 b) ↔ r a b},
  { toEquiv := toEquiv, map_rel_iff' := map_rel_iff' } = { toEquiv := toEquiv_1, map_rel_iff' := map_rel_iff'_1 } →
    toEquiv = toEquiv_1
-- Init.Data.UInt.Bitwise
UInt8.toUInt32_xor : ∀ (a b : UInt8), (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- `Ideal.sum_ramification_inertia`, in the local (DVR) case.  -/
Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing : ∀ {R : Type u} [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  (K : Type u_1) (L : Type u_2) [inst_4 : Field K] [inst_5 : Field L] [IsDedekindDomain R] [inst_7 : Algebra R K]
  [IsFractionRing R K] [inst_9 : Algebra S L] [IsFractionRing S L] [inst_11 : Algebra K L] [inst_12 : Algebra R L]
  [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [inst_16 : IsLocalRing S] {p : Ideal R} [p.IsMaximal],
  p ≠ ⊥ →
    p.ramificationIdx' (IsLocalRing.maximalIdeal S) * p.inertiaDeg' (IsLocalRing.maximalIdeal S) = Module.finrank K L
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.modulus_mul_add : ∀ {m a b : ℕ}, m * a + b ≡ b [MOD m]
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.disjoint_edges_takeUntil_dropUntil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {x : V} {w : G.Walk u v},
  w.IsTrail → ∀ (hx : x ∈ w.support), (w.takeUntil x hx).edges.Disjoint (w.dropUntil x hx).edges
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.Full.mapCommGrp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} [inst_6 : F.Braided] [F.Full] [F.Faithful], F.mapCommGrp.Full
-- Mathlib.Algebra.GroupWithZero.Basic
/-- An element is said to be nilpotent if some natural-number-power of it equals zero.

Note that we require only the bare minimum assumptions for the definition to make sense. Even
`MonoidWithZero` is too strong since nilpotency is important in the study of rings that are only
power-associative.  -/
IsNilpotent : {R : Type u_3} → [Zero R] → [Pow R ℕ] → R → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.relStructSuccEquivMulStruct_symm_apply_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n}
  (h : g.MulStruct SSet.RelativeMorphism.const f i), (SSet.PtSimplex.relStructSuccEquivMulStruct.symm h).map = h.map
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isPairSelfAdjoint_equiv : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₂] {B F : M →ₗ[R] M →ₗ[R] M₂} (e : M₁ ≃ₗ[R] M) (f : Module.End R M),
  B.IsPairSelfAdjoint F ⇑f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) ⇑(e.symm.conj f)
-- Mathlib.Order.Lattice
inf_eq_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = a ↔ a ≤ b
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSlice.instToIterator : {α : Type u_1} →
  [inst : Ord α] →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RcoSliceData α)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxoIterator α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure b.fst)
      α
-- Mathlib.Data.PEquiv
PEquiv.trans_symm_eq_iff_forall_isSome : ∀ {α : Type u} {β : Type v} {f : α ≃. β}, f.trans f.symm = PEquiv.refl α ↔ ∀ (a : α), (f a).isSome = true
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearEquiv.trans_dualMap_symm_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M),
  ↑(e ≪≫ₗ e.flip.symm.dualMap) = Module.Dual.eval R N
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.isSwap_iff_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.IsSwap ↔ σ.cycleType = {2}
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularRing.toIsNoetherian : ∀ {R : Type u_2} {inst : CommRing R} [self : IsRegularRing R], IsNoetherian R R
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.neg : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {b : m → α} [inst : LT α] [inst_1 : NegZeroClass R] {M : Matrix m m R},
  M.BlockTriangular b → (-M).BlockTriangular b
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_attach_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : CommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N},
  ∏ x ∈ s.attach, h (↑x) (f ↑x) = ∏ x ∈ s, h x (f x)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.PreSubmersivePresentation.ofHasCoeffs_map : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (P : Algebra.PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (a : σ),
  (P.ofHasCoeffs R₀).map a = P.map a
-- Mathlib.Combinatorics.Derangements.Basic
derangements.Equiv.RemoveNone.mem_fiber : ∀ {α : Type u_1} [inst : DecidableEq α] (a : Option α) (f : Equiv.Perm α),
  f ∈ derangements.Equiv.RemoveNone.fiber a ↔ ∃ F ∈ derangements (Option α), F none = a ∧ Equiv.removeNone F = f
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hasForgetToLat : CategoryTheory.HasForget₂ HeytAlg BddDistLat
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.isBipartite : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → G.IsBipartite
-- Mathlib.Topology.Separation.Basic
t0Space_of_injective_of_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Function.Injective f → Continuous f → ∀ [T0Space Y], T0Space X
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : (t.getKey? a).isSome = true}, (t.getKey? a).get h = t.getKey a ⋯
-- Mathlib.Algebra.Order.Group.PosPart
/-- See also `negPart_eq_zero`.  -/
negPart_eq_zero' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, a⁻ = 0 ↔ -a ≤ 0
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_le_iff_le_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N} {S : AddSubsemigroup M}
  {T : AddSubsemigroup N}, AddSubsemigroup.map f S ≤ T ↔ S ≤ AddSubsemigroup.comap f T
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The comultiplication 2-morphism of the comonad.  -/
CategoryTheory.Bicategory.Comonad.comul : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a : B} → {t : a ⟶ a} → [CategoryTheory.Bicategory.Comonad t] → t ⟶ CategoryTheory.CategoryStruct.comp t t
-- Mathlib.Analysis.MeanInequalitiesPow
NNReal.rpow_add_le_add_rpow : ∀ {p : ℝ} (a b : NNReal), 0 ≤ p → p ≤ 1 → (a + b) ^ p ≤ a ^ p + b ^ p
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_mem_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  a ∈ t.insert k → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instZero : {α : Type u_1} → [AddCommGroup α] → [inst : Preorder α] → Zero (LowerSet α)
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.CodescendsAlong.of_isPushout : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P Q : CategoryTheory.MorphismProperty C}
  [self : P.CodescendsAlong Q] {Z X Y A : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A},
  CategoryTheory.IsPushout f g inl inr → Q f → P inl → P g
-- Mathlib.RingTheory.Localization.Module
LinearIndependent.of_isLocalizedModule_of_isRegular : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_3} {Mₛ : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid Mₛ] [inst_4 : Module R Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f]
  {ι : Type u_5} {v : ι → M}, LinearIndependent R v → (∀ (s : ↥S), IsRegular ↑s) → LinearIndependent R (⇑f ∘ v)
-- Mathlib.Data.TypeVec
TypeVec.dropFun_diag : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)}, TypeVec.dropFun TypeVec.prod.diag = TypeVec.prod.diag
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁ : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive] (n : ℤ)
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCommShiftIso n).hom.app X).hom₁ = (CategoryTheory.Functor.commShiftIso F n).hom.app X.obj₁
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.Context : Type
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.hom_inv_id : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d),
  CategoryTheory.CategoryStruct.comp f.hom.hom f.inv.hom = CategoryTheory.CategoryStruct.id c.pt
-- Init.Data.Int.Order
Int.min_le_right : ∀ (a b : ℤ), min a b ≤ b
-- Mathlib.Data.FinEnum
_private.Mathlib.Data.FinEnum.0.FinEnum.Finset.enum.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_1 ()
-- Mathlib.Logic.Equiv.PartialEquiv
/-- **Alias** of the reverse direction of `PartialEquiv.IsImage.iff_preimage_eq`. -/
PartialEquiv.IsImage.of_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.source ∩ ↑e ⁻¹' t = e.source ∩ s → e.IsImage s t
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_pow_odd : ∀ (n : ℕ), ∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ (2 * n + 1) = 2 * ∏ i ∈ Finset.range n, (2 * ↑i + 2) / (2 * ↑i + 3)