mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.FunProp.Mor
/-- Morphism application  -/
Mathlib.Meta.FunProp.Mor.App : Type
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.image_mem_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F},
  ApproximatesLinearOn f f' s c →
    ∀ (f'symm : f'.NonlinearRightInverse) {x : E},
      s ∈ nhds x → Subsingleton F ∨ c < f'symm.nnnorm⁻¹ → f '' s ∈ nhds (f x)
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.instInhabitedCasesEntry : Inhabited Lean.Meta.Grind.CasesEntry
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- We say that an adjunction `F ⊣ G` is triangulated if it is compatible with the `CommShift`
structures on `F` and `G` (in the sense of `Adjunction.CommShift`) and if both `F` and `G`
are triangulated functors.
 -/
CategoryTheory.Adjunction.IsTriangulated : {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.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.Limits.HasZeroObject D] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : CategoryTheory.Preadditive D] →
                [inst_6 : CategoryTheory.HasShift C ℤ] →
                  [inst_7 : CategoryTheory.HasShift D ℤ] →
                    [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                      [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                        [CategoryTheory.Pretriangulated C] →
                          [CategoryTheory.Pretriangulated D] →
                            {F : CategoryTheory.Functor C D} →
                              {G : CategoryTheory.Functor D C} → (F ⊣ G) → [F.CommShift ℤ] → [G.CommShift ℤ] → Prop
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertManyIfNewUnit_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {ρ : Type w} [inst : ForIn Id ρ α] {motive : Std.HashMap α Unit → Prop}
  (m : Std.HashMap α Unit) (l : ρ),
  motive m →
    (∀ (m : Std.HashMap α Unit) (a : α), motive m → motive (m.insertIfNew a ())) → motive (m.insertManyIfNewUnit l)
-- Std.Time.Format.Modifier
Std.Time.Modifier.K.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.K presentation = Std.Time.Modifier.K presentation_1 → presentation = presentation_1
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_comp_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P), (Monoid.Coprod.lift f g).comp Monoid.Coprod.inr = g
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.forgetCocone_pt : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T), (CategoryTheory.Over.forgetCocone X).pt = X
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheoremTypeCore?.mkArgs2.match_1.splitter : (motive : Lean.Expr → Sort u_1) →
  (__x : Lean.Expr) →
    ((n : Lean.Name) →
        (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE n d b binderInfo)) →
      ((x : Lean.Expr) →
          (∀ (n : Lean.Name) (d b : Lean.Expr) (binderInfo : Lean.BinderInfo),
              x = Lean.Expr.forallE n d b binderInfo → False) →
            motive x) →
        motive __x
-- Mathlib.Data.Finsupp.Basic
/-- `Finsupp.sumElim f g` maps `inl x` to `f x` and `inr y` to `g y`.  -/
Finsupp.sumElim : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → [inst : Zero γ] → (α →₀ γ) → (β →₀ γ) → α ⊕ β →₀ γ
-- Mathlib.Data.Int.Cast.Lemmas
MonoidWithZeroHom.ext_int_iff : ∀ {M : Type u_5} [inst : MonoidWithZero M] {f g : ℤ →*₀ M},
  f = g ↔ f (-1) = g (-1) ∧ f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opENorm_lsmul : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : NormSMulClass R E] [inst_7 : IsScalarTower 𝕜 R E] [Nontrivial E],
  ‖ContinuousLinearMap.lsmul 𝕜 R‖ₑ = 1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A} (hG₀ : CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G))
  (hG : (X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index G)) (a : S.Arrow) {Z : A} (h : G.obj (Opposite.op a.Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift✝ hG₀ hG s)
      (CategoryTheory.CategoryStruct.comp (G.map a.f.op) h) =
    CategoryTheory.CategoryStruct.comp (s.ι a) h
-- Init.Data.String.Basic
String.Slice.Pos.slice_ofSlice : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos},
  (String.Slice.Pos.ofSlice pos).slice p₀ p₁ ⋯ ⋯ = pos
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.sInf_ringCon : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] (S : Set (TwoSidedIdeal R)),
  (sInf S).ringCon = sInf (TwoSidedIdeal.ringCon '' S)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.forIn_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {b : δ} {f : α × β → δ → m (ForInStep δ)},
  t₁.Equiv t₂ → forIn t₁ b f = forIn t₂ b f
-- Mathlib.Analysis.Calculus.FDeriv.Norm
HasFDerivAt.hasFDerivAt_norm_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ},
  t ≠ 0 → HasFDerivAt (fun x => ‖x‖) f x → HasFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)
-- Mathlib.Algebra.Ring.Shrink
Shrink.instNonUnitalNonAssocSemiring : {α : Type u_1} →
  [inst : Small.{v, u_1} α] → [NonUnitalNonAssocSemiring α] → NonUnitalNonAssocSemiring (Shrink.{v, u_1} α)
-- Mathlib.Order.Heyting.Basic
compl_sup_distrib : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a b : α), (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
-- Mathlib.Data.Fin.Fin2
/-- Define a dependent function on `Fin2 (succ n)` by giving its value at
zero (`H1`) and by giving a dependent function on the rest (`H2`).  -/
Fin2.cases' : {n : ℕ} → {C : Fin2 n.succ → Sort u} → C Fin2.fz → ((n_1 : Fin2 n) → C n_1.fs) → (i : Fin2 n.succ) → C i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_erase_eq_iff_not_compare_eq_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (t.erase k).max he = t.max ⋯ ↔ ¬cmp k (t.max ⋯) = Ordering.eq
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.outer_trim : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) [OrderTopology R]
  [CompactIccSpace R] [inst_4 : MeasurableSpace R] [BorelSpace R] [DenselyOrdered R], f.outer.trim = f.outer
-- Mathlib.Analysis.Distribution.DerivNotation
LineDerivSMul.mk : ∀ {R : Type u_11} {V : Type u} {E : Type v} {F : outParam (Type w)} [inst : SMul R E] [inst_1 : SMul R F]
  [inst_2 : LineDeriv V E F],
  (∀ (v : V) (r : R) (x : E), LineDeriv.lineDerivOp v (r • x) = r • LineDeriv.lineDerivOp v x) → LineDerivSMul R V E F
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instFunLike : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → {ι : Type u_7} → FunLike (M [⋀^ι]→ₗ[R] N) (ι → M) N
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
ClosedEmbeddingContinuousFunctionalCalculus.congr_simp : ∀ (R : Type u_1) (A : Type u_2) (p p_1 : A → Prop),
  p = p_1 →
    ∀ [inst : CommSemiring 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],
      ClosedEmbeddingContinuousFunctionalCalculus R A p = ClosedEmbeddingContinuousFunctionalCalculus R A p_1
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGE_map_ofDual`. -/
List.SortedGE.map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.ofDual) l).SortedGE → l.SortedLE
-- Mathlib.GroupTheory.Congruence.Defs
/-- Extensionality rule for congruence relations.  -/
Con.ext : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, (∀ (x y : M), c x y ↔ d x y) → c = d
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_cons : ∀ {α : Type u_1} (x : α) (xs : List α), FreeAddMonoid.ofList (x :: xs) = FreeAddMonoid.of x + FreeAddMonoid.ofList xs
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.eval_nondegenerate : ∀ {K : Type u_1} {V : Type u_2} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], (Module.Dual.eval K V).Nondegenerate
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_eq_pow_card : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} {b : M},
  (∀ a ∈ s, f a = b) → ∏ a ∈ s, f a = b ^ s.card
-- Mathlib.Algebra.Free
FreeSemigroup.instInhabited.eq_1 : ∀ {α : Type u} [inst : Inhabited α], FreeSemigroup.instInhabited = { default := FreeSemigroup.of default }
-- Mathlib.Dynamics.Transitive
/-- An action of a monoid `M` on `α` is topologically transitive if and only if for any nonempty
open subset `U` of `α` the union of the preimages of `U` over the elements of `M` is dense in `α`.
 -/
MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α],
  MulAction.IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, (fun x => m • x) ⁻¹' U)
-- Std.Async.Basic
Std.Async.MaybeTask.instMonad : Monad Std.Async.MaybeTask
-- Mathlib.LinearAlgebra.Prod
/-- `N` as a submodule of `M × N` is isomorphic to `N`.  -/
Submodule.sndEquiv : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] → [inst_4 : Module R M₂] → ↥(Submodule.snd R M M₂) ≃ₗ[R] M₂
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_inj : ∀ {R : Type u} [inst : Semiring R] {a b : Polynomial R}, a.toFinsupp = b.toFinsupp ↔ a = b
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.isEquivalenceMapPair : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] {F : CategoryTheory.Functor C C'} {F' : CategoryTheory.Functor D D'}
  [F.IsEquivalence] [F'.IsEquivalence], (CategoryTheory.Join.mapPair F F').IsEquivalence
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_part_iff_part_eq_part : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a b : α},
  a ∈ s → b ∈ s → (a ∈ P.part b ↔ P.part a = P.part b)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.category : CategoryTheory.SmallCategory CategoryTheory.Limits.WalkingReflexivePair
-- Mathlib.Algebra.Order.Positive.Ring
Positive.val_pow : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (x : { x // 0 < x })
  (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_f_descCochain_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n)
  (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p₁)
      ((CochainComplex.mappingCone.descCochain φ α β h).v p₁ p₂ h₁₂) =
    β.v p₁ p₂ h₁₂
-- Lean.Attributes
Lean.AttributeExtensionState.mk.injEq : ∀ (newEntries : List Lean.AttributeExtensionOLeanEntry) (map : Std.HashMap Lean.Name Lean.AttributeImpl)
  (newEntries_1 : List Lean.AttributeExtensionOLeanEntry) (map_1 : Std.HashMap Lean.Name Lean.AttributeImpl),
  ({ newEntries := newEntries, map := map } = { newEntries := newEntries_1, map := map_1 }) =
    (newEntries = newEntries_1 ∧ map = map_1)
-- Init.Data.UInt.Lemmas
USize.sub_eq_add_mul : ∀ (a b : USize), a - b = a + USize.ofNatLT (USize.size - 1) ⋯ * b
-- Init.Data.String.PosRaw
String.Pos.Raw.offsetBy_zero_left : ∀ {p : String.Pos.Raw}, String.Pos.Raw.offsetBy 0 p = p
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A `c : Bicone F` is:
* an object `c.pt` and
* morphisms `π j : pt ⟶ F j` and `ι j : F j ⟶ pt` for each `j`,
* such that `ι j ≫ π j'` is the identity when `j = j'` and zero otherwise.
 -/
CategoryTheory.Limits.Bicone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [CategoryTheory.Limits.HasZeroMorphisms C] → (J → C) → Type (max (max uC uC') w)
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the inverse direction of the isomorphism
`PreservesLimit₂.isoObjConePointsOfIsLimit` w.r.t. the canonical maps to the limit.  -/
CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsColimit_inv_comp_map_π : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cone K₁}
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone K₂} (hc₂ : CategoryTheory.Limits.IsLimit c₂)
  {c₃ :
    CategoryTheory.Limits.Cone
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
  (hc₃ : CategoryTheory.Limits.IsLimit c₃) (j : J₁ × J₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimit₂.isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).inv
      (CategoryTheory.CategoryStruct.comp ((G.map (c₁.π.app j.1)).app c₂.pt)
        ((G.obj (K₁.obj j.1)).map (c₂.π.app j.2))) =
    c₃.π.app j
-- Mathlib.Order.WithBot
WithBot.exists_ne_bot : ∀ {α : Type u_1} {p : WithBot α → Prop}, (∃ x, x ≠ ⊥ ∧ p x) ↔ ∃ x, p ↑x
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.le_trailingDegree_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
-- Mathlib.Tactic.Sat.FromLRAT
/-- Constructs the formula expression from the input CNF, as a balanced tree of `Fmla.and` nodes.  -/
Mathlib.Tactic.Sat.buildConj : Array (Array ℤ) → ℕ → ℕ → Lean.Expr
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.del : ∀ {α : Type u_1} {c₀ : RBTree.RBColor} {n₀ : ℕ} {c : RBTree.RBColor} {n : ℕ} {c' : RBTree.RBColor} {t : RBTree.RBNode α}
  {path : RBTree.RBNode.Path α},
  RBTree.RBNode.Path.Balanced c₀ n₀ path c n →
    RBTree.RBNode.DelProp c' t n →
      (c = RBTree.RBColor.black → c' ≠ RBTree.RBColor.red) → ∃ n, (path.del t c').Balanced RBTree.RBColor.black n
-- Mathlib.Data.Fin.Tuple.Basic
/-- A property holds for all dependent finite sequence of length m + n iff
it holds for the concatenation of all pairs of length m sequences and length n sequences.  -/
Fin.forall_fin_add_pi : ∀ {m n : ℕ} {γ : Fin (m + n) → Sort u_3} {P : ((i : Fin (m + n)) → γ i) → Prop},
  (∀ (v : (i : Fin (m + n)) → γ i), P v) ↔
    ∀ (vₘ : (i : Fin m) → γ (Fin.castAdd n i)) (vₙ : (j : Fin n) → γ (Fin.natAdd m j)), P fun i => Fin.addCases vₘ vₙ i
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
HomologicalComplex.restrictionXIso.hcongr_13 : ∀ (ι ι' : Type u_1),
  ι = ι' →
    ∀ (ι'_1 ι'' : Type u_2),
      ι'_1 = ι'' →
        ∀ (c : ComplexShape ι) (c' : ComplexShape ι'),
          c ≍ c' →
            ∀ (c'_1 : ComplexShape ι'_1) (c'' : ComplexShape ι''),
              c'_1 ≍ c'' →
                ∀ (C C' : Type u_3),
                  C = C' →
                    ∀ (inst : CategoryTheory.Category.{v_1, u_3} C) (inst' : CategoryTheory.Category.{v_1, u_3} C'),
                      inst ≍ inst' →
                        ∀ (inst_1 : CategoryTheory.Limits.HasZeroMorphisms C)
                          (inst'_1 : CategoryTheory.Limits.HasZeroMorphisms C'),
                          inst_1 ≍ inst'_1 →
                            ∀ (K : HomologicalComplex C c'_1) (K' : HomologicalComplex C' c''),
                              K ≍ K' →
                                ∀ (e : c.Embedding c'_1) (e' : c'.Embedding c''),
                                  e ≍ e' →
                                    ∀ (inst_2 : e.IsRelIff) (inst'_2 : e'.IsRelIff),
                                      inst_2 ≍ inst'_2 →
                                        ∀ (i : ι) (i' : ι'),
                                          i ≍ i' →
                                            ∀ (i'_1 : ι'_1) (i'' : ι''),
                                              i'_1 ≍ i'' →
                                                ∀ (h : e.f i = i'_1) (h' : e'.f i' = i''),
                                                  h ≍ h' → K.restrictionXIso e h ≍ K'.restrictionXIso e' h'
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `mfderiv` using the custom elaborator, and special-casing
arguments that can use the `T%` elaborator.  -/
Manifold.delabMFDeriv : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Order.Compact
IsCompact.exists_sSup_image_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [inst_2 : TopologicalSpace β] [ClosedIciTopology α] {s : Set β},
  IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, sSup (f '' s) = f x
-- Mathlib.Data.Nat.Squarefree
Squarefree.natFactorization_le_one : ∀ {n : ℕ} (p : ℕ), Squarefree n → n.factorization p ≤ 1
-- Lean.Meta.Basic
Lean.Meta.Cache.funInfo : Lean.Meta.Cache → Lean.Meta.FunInfoCache
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.anyM.eq_1 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool), List.anyM p [] = pure false
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t'_jii : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J),
  D.t' j i i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j i))
      (CategoryTheory.CategoryStruct.comp (D.t j i)
        (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd (D.f i i) (D.f i j))))
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse.  -/
Orientation.norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle (x + y) y).cos = ‖x + y‖
-- Init.Data.Vector.Lemmas
Vector.replicate_succ : ∀ {n : ℕ} {α : Type u_1} {a : α}, Vector.replicate (n + 1) a = (Vector.replicate n a).push a
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `s` be an `R`-algebra isomorphism. Then `s x` is a conjugate root of `x`.
 -/
isConjRoot_of_algEquiv : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A) (s : A ≃ₐ[R] A),
  IsConjRoot R x (s x)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.comap_comap : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  [inst_2 : BooleanAlgebra γ] (L : BooleanSubalgebra γ) (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β),
  BooleanSubalgebra.comap f (BooleanSubalgebra.comap g L) = BooleanSubalgebra.comap (g.comp f) L
-- Mathlib.Topology.Constructions
Pi.induced_domRestrict_sUnion : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (𝔖 : Set (Set ι)),
  TopologicalSpace.induced (⋃₀ 𝔖).domRestrict Pi.topologicalSpace =
    ⨅ S ∈ 𝔖, TopologicalSpace.induced S.domRestrict Pi.topologicalSpace
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.eq_4 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_4 ()
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_hom_homOfLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U V : X.Opens) (e : U ≤ V),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f U).hom (Y.homOfLE ⋯) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE e) (AlgebraicGeometry.Scheme.Hom.isoImage f V).hom
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If `P` is a sheaf for the sieve `S` on `X`, then if two natural transformations from `yoneda.obj X`
to `P` agree when restricted to the subfunctor given by `S`, they are equal.
 -/
CategoryTheory.Presieve.IsSheafFor.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
  CategoryTheory.Presieve.IsSheafFor P S.arrows →
    ∀ (t₁ t₂ : CategoryTheory.yoneda.obj X ⟶ P),
      CategoryTheory.CategoryStruct.comp S.functorInclusion t₁ =
          CategoryTheory.CategoryStruct.comp S.functorInclusion t₂ →
        t₁ = t₂
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.A₁B₀_commutes : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → A₁ * B₀ = B₀ * A₁
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The terms corresponding to the `⁅H, H⁆`-relations.  -/
CartanMatrix.Relations.HH : (R : Type u) → {B : Type v} → [inst : CommRing R] → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)