mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Basic
strictAntiOn_inv_pos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀],
  StrictAntiOn (fun x => x⁻¹) {r | 0 < r}
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstLTInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- Any pseudofunctor from a (2,1)-category to a bicategory factors through
the pith of the target bicategory.  -/
CategoryTheory.Bicategory.Pith.pseudofunctorToPith : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {B' : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory B'] →
        [CategoryTheory.Bicategory.IsLocallyGroupoid B'] →
          CategoryTheory.Pseudofunctor B' B → CategoryTheory.Pseudofunctor B' (CategoryTheory.Bicategory.Pith B)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.id_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : A),
  (AlgHom.id R A) p = p
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem_append_right : ∀ {i : ℕ} {a b : ByteArray} {h : i < (a ++ b).size} (hle : a.size ≤ i), (a ++ b)[i] = b[i - a.size]
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.left'_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.MonoidalCoherence X Y],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCoherence.iso ≪≫ (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).symm
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.πE_ιE : ∀ {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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_ιE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_ιE._auto_3),
  CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) =
    CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁) (X.pOpcycles f₂ f₃ n₁)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Topology.IsQuotientMap ⇑h
-- Mathlib.NumberTheory.ZetaValues
/-- Explicit formula for `L(χ, 3)`, where `χ` is the unique nontrivial Dirichlet character modulo 4.
 -/
hasSum_L_function_mod_four_eval_three : HasSum (fun n => 1 / ↑n ^ 3 * Real.sin (Real.pi * ↑n / 2)) (Real.pi ^ 3 / 32)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.le_map_of_comap_le_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {I : Ideal R} {K : Ideal S} [inst_3 : RingHomClass F R S],
  Function.Surjective ⇑f → Ideal.comap f K ≤ I → K ≤ Ideal.map f I
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Reflecting colimits at any universe implies reflecting colimits at universe `0`.  -/
CategoryTheory.Limits.reflectsSmallestColimits_of_reflectsColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
instConditionallyCompleteLinearOrderWithTop : {α : Type u_1} → [ConditionallyCompleteLinearOrder α] → ConditionallyCompleteLinearOrder (WithTop α)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoZero'_eq_isoZero : ∀ {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] (F : CategoryTheory.Functor C D) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A],
  CategoryTheory.Functor.CommShift.isoZero' F A 0 ⋯ = CategoryTheory.Functor.CommShift.isoZero F A
-- Init.Data.Array.Lemmas
Array.map_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {xs : Array α}, Array.map f xs = Array.map g xs ↔ ∀ a ∈ xs, f a = g a
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.ι_def : ∀ (R : Type u_3) {X : Type u_4} [inst : CommSemiring R] (m : X),
  FreeAlgebra.ι R m = Quot.mk (FreeAlgebra.Rel R X) (FreeAlgebra.Pre.of m)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- a first integer  -/
CochainComplex.HomComplex.Triplet.p : {n : ℤ} → CochainComplex.HomComplex.Triplet n → ℤ
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.symm_p_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] {Z : C} (h : A ⨯ A ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.symm.p h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom) h
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, (t.alter k f).contains k = (f t[k]?).isSome
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- Given submodules `p ⊆ M`, `p₂ ⊆ M₂`, `p₃ ⊆ M₃` and maps `f : M → M₂`, `g : M₂ → M₃` inducing
`mapQ f : M ⧸ p → M₂ ⧸ p₂` and `mapQ g : M₂ ⧸ p₂ → M₃ ⧸ p₃` then
`mapQ (g ∘ f) = (mapQ g) ∘ (mapQ f)`.  -/
Submodule.mapQ_comp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {R₃ : Type u_5} {M₃ : Type u_6} [inst_6 : Ring R₃] [inst_7 : AddCommGroup M₃] [inst_8 : Module R₃ M₃]
  (p₂ : Submodule R₂ M₂) (p₃ : Submodule R₃ M₃) {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃}
  [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p ≤ Submodule.comap f p₂)
  (hg : p₂ ≤ Submodule.comap g p₃) (h : optParam (p ≤ Submodule.comap f (Submodule.comap g p₃)) ⋯),
  p.mapQ p₃ (g ∘ₛₗ f) h = p₂.mapQ p₃ g hg ∘ₛₗ p.mapQ p₂ f hf
-- Mathlib.GroupTheory.Nilpotent
Subgroup.derived_le_lower_central : ∀ {G : Type u_1} [inst : Group G] (n : ℕ), derivedSeries G n ≤ ⊤.lowerCentralSeries n
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- We say that `f : SmoothBumpCovering ι I M s` is *subordinate* to a map `U : M → Set M` if for each
index `i`, we have `tsupport (f i) ⊆ U (f i).c`. This notion is a bit more general than
being subordinate to an open covering of `M`, because we make no assumption about the way `U x`
depends on `x`.
 -/
SmoothBumpCovering.IsSubordinate : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    [inst_5 : FiniteDimensional ℝ E] → {s : Set M} → SmoothBumpCovering ι I M s → (M → Set M) → Prop
-- Mathlib.Computability.Reduce
disjoin_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, Sum.elim p q ≤₀ r ↔ p ≤₀ r ∧ q ≤₀ r
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.State.mk.sizeOf_spec : ∀ (toDerive : Lean.NameMap Lean.ExprSet) (toOmit : Array (Lean.Ident × Lean.Name)),
  sizeOf { toDerive := toDerive, toOmit := toOmit } = 1 + sizeOf toDerive + sizeOf toOmit
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_eq_cfcₙHom_of_cfcHom : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p]
  [ContinuousMapZero.UniqueHom R A] {a : A} (ha : p a), cfcₙHom ha = cfcₙHom_of_cfcHom R ha
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
RingEquiv.sofLeftInverse'_symm_apply : ∀ {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] {g : S → R} {f : F} (h : Function.LeftInverse g ⇑f)
  (x : ↥(NonUnitalRingHom.srange f)), (RingEquiv.sofLeftInverse' h).symm x = g ↑x
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.subAddAction.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] (n : ℕ) [inst_2 : DecidableEq α],
  Set.powersetCard.subAddAction G α n = { carrier := Set.powersetCard α n, vadd_mem' := ⋯ }
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.map_normal : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal],
  (Subgroup.map (QuotientGroup.mk' N) M).Normal
-- Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
/-- Given candidate data for an exact pairing,
which is sent by a faithful monoidal functor to an exact pairing,
the equations holds automatically.  -/
CategoryTheory.ExactPairing.ofFaithful : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.Monoidal] →
                [F.Faithful] →
                  {X Y : C} →
                    (eval :
                        CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶
                          CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →
                      (coeval :
                          CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶
                            CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) →
                        [inst_6 : CategoryTheory.ExactPairing (F.obj X) (F.obj Y)] →
                          F.map eval =
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F Y X)
                                (CategoryTheory.CategoryStruct.comp (ε_ (F.obj X) (F.obj Y))
                                  (CategoryTheory.Functor.LaxMonoidal.ε F)) →
                            F.map coeval =
                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F)
                                  (CategoryTheory.CategoryStruct.comp (η_ (F.obj X) (F.obj Y))
                                    (CategoryTheory.Functor.LaxMonoidal.μ F X Y)) →
                              CategoryTheory.ExactPairing X Y
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasAntitoneBasis.prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_6} [inst : LinearOrder ι] {f : Filter α} {g : Filter β} {s : ι → Set α}
  {t : ι → Set β}, f.HasAntitoneBasis s → g.HasAntitoneBasis t → (f ×ˢ g).HasAntitoneBasis fun n => s n ×ˢ t n
-- Mathlib.Algebra.Group.Opposite
MulOpposite.unop_pow : ∀ {α : Type u_1} [inst : Monoid α] (x : αᵐᵒᵖ) (n : ℕ), MulOpposite.unop (x ^ n) = MulOpposite.unop x ^ n
-- Mathlib.Topology.Algebra.MulAction
IsCompact.smul_set : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X] {k : Set M} {u : Set X}, IsCompact k → IsCompact u → IsCompact (k • u)
-- Mathlib.RingTheory.PrincipalIdealDomain
isCoprime_of_prime_dvd : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {x y : R},
  ¬(x = 0 ∧ y = 0) → (∀ (z : R), Prime z → z ∣ x → ¬z ∣ y) → IsCoprime x y
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_4 : HSub Std.Time.Nanosecond.Offset Std.Time.Day.Offset Std.Time.Nanosecond.Offset
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqLeanDiagnosticTag.beq : Lean.Lsp.LeanDiagnosticTag → Lean.Lsp.LeanDiagnosticTag → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → Std.DHashMap.Const.get? (m₁.inter m₂) k = none
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Traversal.0.SimpleGraph.Walk.getVert.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) (v v_1 : V)
  (h : G.Adj u v_1) (p : G.Walk v_1 v) (h_1 : (x : ℕ) → motive u SimpleGraph.Walk.nil x)
  (h_2 : (v v_2 : V) → (h : G.Adj u v_2) → (p : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons h p) 0)
  (h_3 : (v v_2 : V) → (h : G.Adj u v_2) → (q : G.Walk v_2 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ),
  (match v, SimpleGraph.Walk.cons h p, 0 with
    | .(u), SimpleGraph.Walk.nil, x => h_1 x
    | v, SimpleGraph.Walk.cons h p, 0 => h_2 v v_2 h p
    | v, SimpleGraph.Walk.cons h q, n.succ => h_3 v v_2 h q n) =
    h_2 v v_1 h p
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_eq_zero_iff : ∀ {n : Int16}, n.toNatClampNeg = 0 ↔ n ≤ 0
-- Init.Data.UInt.Bitwise
UInt32.ofNat_or : ∀ (a b : ℕ), UInt32.ofNat (a ||| b) = UInt32.ofNat a ||| UInt32.ofNat b
-- Mathlib.NumberTheory.FLT.Four
Int.isCoprime_of_sq_sum : ∀ {r s : ℤ}, IsCoprime s r → IsCoprime (r ^ 2 + s ^ 2) r
-- Mathlib.Algebra.Homology.Homotopy
/-- An auxiliary construction for `mkInductive`.

Here we build by induction a family of diagrams,
but don't require at the type level that these successive diagrams actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy)
in `mkInductive`.

At this stage, we don't check the homotopy condition in degree 0,
because it "falls off the end", and is easier to treat using `xNext` and `xPrev`,
which we do in `mkInductiveAux₂`.
 -/
Homotopy.mkInductiveAux₁ : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {P Q : ChainComplex V ℕ} →
        (e : P ⟶ Q) →
          (zero : P.X 0 ⟶ Q.X 1) →
            (one : P.X 1 ⟶ Q.X 2) →
              e.f 1 =
                  CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1) →
                ((n : ℕ) →
                    (p :
                        (f : P.X n ⟶ Q.X (n + 1)) ×'
                          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                            e.f (n + 1) =
                              CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                                CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
                      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
                        e.f (n + 2) =
                          CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
                            CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) →
                  (n : ℕ) →
                    (f : P.X n ⟶ Q.X (n + 1)) ×'
                      (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                        e.f (n + 1) =
                          CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                            CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))
-- Mathlib.Algebra.Free
FreeSemigroup.instInhabited : {α : Type u} → [Inhabited α] → Inhabited (FreeSemigroup α)
-- Mathlib.Data.UInt
UInt8.toBitVec_intCast : ∀ (z : ℤ), (↑z).toBitVec = ↑z
-- Init.Meta.Defs
Lean.Meta.Omega.OmegaConfig.mk.sizeOf_spec : ∀ (splitDisjunctions splitNatSub splitNatAbs splitMinMax : Bool),
  sizeOf
      { splitDisjunctions := splitDisjunctions, splitNatSub := splitNatSub, splitNatAbs := splitNatAbs,
        splitMinMax := splitMinMax } =
    1 + sizeOf splitDisjunctions + sizeOf splitNatSub + sizeOf splitNatAbs + sizeOf splitMinMax
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.app'.sizeOf_spec : ∀ (a a_1 : Mathlib.Tactic.ITauto.Proof), sizeOf (a.app' a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.setIntegral_finset : ∀ {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {f : X → E}
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasurableSingletonClass X] {μ : MeasureTheory.Measure X}
  (s : Finset X), MeasureTheory.IntegrableOn f (↑s) μ → ∫ (x : X) in ↑s, f x ∂μ = ∑ x ∈ s, μ.real {x} • f x
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotate_map_hom₃ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.rotate C).map f).hom₃ = (CategoryTheory.shiftFunctor C 1).map f.hom₁
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.rootForm_pos_of_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] [inst_6 : Module R M]
  [inst_7 : Module R N] (P : RootPairing ι R M N) {x : M}, x ∈ P.rootSpan R → x ≠ 0 → 0 < (P.RootForm x) x
-- Mathlib.RingTheory.PicardGroup
/-- Given `M ⊗[R] N ≃ₗ[R] R`, this is the induced isomorphism `M ≃ₗ[R] Nᵛ`.  -/
Module.Invertible.linearEquivDual : {R : Type u} →
  {M : Type v} →
    {N : Type u_1} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → (TensorProduct R M N ≃ₗ[R] R) → M ≃ₗ[R] Module.Dual R N
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
/-- Restriction of scalars for a root pairing taking values in a subfield.

See also `RootPairing.restrictScalars`.  -/
RootPairing.restrictScalars' : {ι : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Field L] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : Module L M] →
                [inst_4 : Module L N] →
                  (P : RootPairing ι L M N) →
                    (K : Type u_5) →
                      [inst_5 : Field K] →
                        [inst_6 : Algebra K L] →
                          [inst_7 : Module K M] →
                            [inst_8 : Module K N] →
                              [IsScalarTower K L M] →
                                [IsScalarTower K L N] →
                                  [P.IsBalanced] →
                                    [P.IsValuedIn K] →
                                      RootPairing ι K ↥(Submodule.span K (Set.range ⇑P.root))
                                        ↥(Submodule.span K (Set.range ⇑P.coroot))
-- Plausible.Testable
Plausible.Testable.subtypeVarTestable : {var : String} →
  {α : Type u} →
    {p β : α → Prop} →
      [(x : α) → Plausible.PrintableProp (p x)] →
        [(x : α) → Plausible.Testable (β x)] →
          [Plausible.SampleableExt (Subtype p)] →
            {var' : String} →
              Plausible.Testable (Plausible.NamedBinder var (∀ (x : α), Plausible.NamedBinder var' (p x → β x)))
-- Mathlib.Algebra.Regular.Basic
IsDedekindFiniteAddMonoid.iff_isAddRightRegular_of_add_eq_zero : ∀ {R : Type u_1} [inst : AddMonoid R], IsDedekindFiniteAddMonoid R ↔ ∀ (x y : R), x + y = 0 → IsAddRightRegular y
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.eq_of_mem_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → q ∈ s → q ∈ as → q = p
-- Mathlib.Topology.List
List.tendsto_nhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} {f : List α → β} {r : List α → Filter β},
  Filter.Tendsto f (pure []) (r []) →
    (∀ (l : List α) (a : α),
        Filter.Tendsto f (nhds l) (r l) → Filter.Tendsto (fun p => f (p.1 :: p.2)) (nhds a ×ˢ nhds l) (r (a :: l))) →
      ∀ (l : List α), Filter.Tendsto f (nhds l) (r l)
-- Mathlib.Order.Antichain
IsAntichain.isWeakAntichain : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)},
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → IsWeakAntichain s
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod_mono : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N],
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) AddSubgroup.prod
    AddSubgroup.prod
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.brecOn.go : {dir : Std.Http.Protocol.H1.Direction} →
  {motive : Std.Http.Protocol.H1.Reader.State dir → Sort u} →
    (t : Std.Http.Protocol.H1.Reader.State dir) →
      ((t : Std.Http.Protocol.H1.Reader.State dir) → Std.Http.Protocol.H1.Reader.State.below t → motive t) →
        motive t ×' Std.Http.Protocol.H1.Reader.State.below t
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
panicking if no such key exists.
 -/
Std.ExtDTreeMap.getKeyGT! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtDTreeMap α β cmp → α → α
-- Mathlib.Data.Real.ConjExponents
Real.holderConjugate_iff : ∀ {p q : ℝ}, p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
-- Batteries.Data.UnionFind.Basic
Batteries.UFNode.mk.injEq : ∀ (parent rank parent_1 rank_1 : ℕ),
  ({ parent := parent, rank := rank } = { parent := parent_1, rank := rank_1 }) = (parent = parent_1 ∧ rank = rank_1)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- A version of `LinearIsometry.adjoint_comp_self` in terms of `LinearMap.adjoint`.  -/
LinearIsometry.adjoint_comp_self' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_5} {E' : Type u_6} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : FiniteDimensional 𝕜 E] [inst_4 : NormedAddCommGroup E']
  [inst_5 : InnerProductSpace 𝕜 E'] [inst_6 : FiniteDimensional 𝕜 E'] (f : E →ₗᵢ[𝕜] E'),
  LinearMap.adjoint f.toLinearMap ∘ₗ f.toLinearMap = LinearMap.id
-- Mathlib.Analysis.Convex.Intrinsic
interior_subset_intrinsicInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, interior s ⊆ intrinsicInterior 𝕜 s
-- Init.Data.List.Range
_private.Init.Data.List.Range.0.List.range'.match_1.eq_2 : ∀ (motive : ℕ → ℕ → ℕ → Sort u_1) (s n step : ℕ) (h_1 : (x x_1 : ℕ) → motive x 0 x_1)
  (h_2 : (s n step : ℕ) → motive s n.succ step),
  (match s, n.succ, step with
    | x, 0, x_1 => h_1 x x_1
    | s, n.succ, step => h_2 s n step) =
    h_2 s n step
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.set_support_zpow_subset : ∀ {α : Type u_1} (p : Equiv.Perm α) (n : ℤ), {x | (p ^ n) x ≠ x} ⊆ {x | p x ≠ x}
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_neg : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (m : M) (r : R), MonoidAlgebra.single m (-r) = -MonoidAlgebra.single m r
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.monomial_mem_nonzeroDivisorsLeft : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {n : σ →₀ ℕ} {r : R},
  (MvPowerSeries.monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisorsLeft R
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_one_div : ∀ {a b : ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  (∀ x ∈ Set.uIcc a b, f x ≠ 0) → ContinuousOn f (Set.uIcc a b) → IntervalIntegrable (fun x => 1 / f x) μ a b