mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Congruence.Hom
/-- The homomorphism on the quotient of a ring by a congruence relation `c`
induced by a homomorphism constant on the equivalence classes of `c`.  -/
RingCon.lift : {M : Type u_1} →
  {P : Type u_3} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring P] → (c : RingCon M) → (f : M →+* P) → c ≤ RingCon.ker f → c.Quotient →+* P
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv_inverse_obj_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (unmop : C),
  ((CategoryTheory.MonoidalOpposite.unmopEquiv C).inverse.obj unmop).unmop = unmop
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_injective_image' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : β → α},
  Function.Injective f →
    ∀ {s : Set β},
      MeasurableSet s → MeasurableSet (f '' s) → MeasureTheory.Measure.count (f '' s) = MeasureTheory.Measure.count s
-- Mathlib.Algebra.Algebra.Basic
FaithfulSMul.algebraMap_eq_zero_iff : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  {r : R}, (algebraMap R A) r = 0 ↔ r = 0
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationBy.structural : Lean.Elab.TerminationBy → Bool
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The **universal property** of the topology on `𝓓^{n}_{K}(E, F)`: a map to `𝓓^{n}_{K}(E, F)`
is continuous if and only if its composition with the structure map
`structureMapCLM ℝ n i : 𝓓^{n}_{K}(E, F) → (E →ᵇ (E [×i]→L[ℝ] F))` is continuous for each
`i ≤ n`.  -/
ContDiffMapSupportedIn.continuous_iff_comp_order_le : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {X : Type u_5} [inst_4 : TopologicalSpace X]
  (φ : X → ContDiffMapSupportedIn E F n K),
  Continuous φ ↔ ∀ (i : ℕ), ↑i ≤ n → Continuous (⇑(ContDiffMapSupportedIn.structureMapCLM ℝ n i) ∘ φ)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.instAddCommGroup : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommRing 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : IsTopologicalAddGroup 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommGroup E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → AddCommGroup (WeakDual 𝕜 E)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_eq_sqrt_one_sub_sin_sq : ∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ Real.pi / 2 → Real.cos x = √(1 - Real.sin x ^ 2)
-- Init.Data.Array.Lemmas
Array.mem_push_self : ∀ {α : Type u_1} {xs : Array α} {x : α}, x ∈ xs.push x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTriangleLTGEOfLE_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (a : ℤ),
  t.natTransTriangleLTGEOfLE a a ⋯ = CategoryTheory.CategoryStruct.id (t.triangleLTGE a)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The inclusion of the image of a morphism into the target.  -/
CategoryTheory.Limits.image.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [inst_1 : CategoryTheory.Limits.HasImage f] → CategoryTheory.Limits.image f ⟶ Y
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.isBasis_of_subset : ∀ {α : Type u_1} {M : Matroid α} {B X : Set α},
  autoParam (X ⊆ M.E) Matroid.IsBase.isBasis_of_subset._auto_1 → M.IsBase B → B ⊆ X → M.IsBasis B X
-- Mathlib.Order.Bounds.Image
StrictMono.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {a : α} {s : Set α},
  StrictMono f → (IsGreatest (f '' s) (f a) ↔ IsGreatest s a)
-- Lean.MetavarContext
/-- Check whether a metavariable is assigned or delayed-assigned. A
delayed-assigned metavariable is already 'solved' but the solution cannot be
substituted yet because we have to wait for some other metavariables to be
assigned first. So in many situations you want to treat a delayed-assigned
metavariable as assigned.
 -/
Lean.MVarId.isAssignedOrDelayedAssigned : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m Bool
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.neg_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.neg.h₂ = -h.h₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α],
  t.WF → t.isEmpty = false → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (compare km k).isLE = true
-- Mathlib.LinearAlgebra.Dimension.Finrank
/-- This is like `rank_eq_one_iff_finrank_eq_one` but works for `2`, `3`, `4`, ...  -/
Module.rank_eq_ofNat_iff_finrank_eq_ofNat : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
  [inst_3 : n.AtLeastTwo], Module.rank R M = OfNat.ofNat n ↔ Module.finrank R M = OfNat.ofNat n
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.toListRev_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} [LawfulMonad m] {xs : Vector β n} {pos : ℕ},
  (xs.iterFromIdxM m pos).toListRev = pure (List.drop pos xs.toList).reverse
-- Init.Data.Int.Order
Int.neg_lt_sub_right_of_lt_add : ∀ {a b c : ℤ}, c < a + b → -b < a - c
-- Mathlib.Algebra.GCDMonoid.Basic
CommGroupWithZero.coe_normUnit : ∀ (G₀ : Type u_2) [inst : CommGroupWithZero G₀] [inst_1 : DecidableEq G₀] {a : G₀}, a ≠ 0 → ↑(normUnit a) = a⁻¹
-- Batteries.Data.List.Basic
/-- Inner loop for `swapAtTR`.  -/
List.swapAtTR.go : {α : Type u_1} → List α → α → List α → ℕ → Array α → α × List α
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.smallSchroder_succ : ∀ {n : ℕ},
  1 < n →
    (n + 1).smallSchroder =
      3 * n.smallSchroder + 2 * ∑ i ∈ Finset.Ioo 0 (n - 1), (i + 1).smallSchroder * (n - i).smallSchroder
-- Lean.Server.Requests
Lean.Server.handleOnDidChange : Lean.Lsp.DidChangeTextDocumentParams → Lean.Server.RequestM Unit
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ (f : α → ENNReal), ∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
-- Mathlib.CategoryTheory.Square
/-- The functor which flips commutative squares.  -/
CategoryTheory.Square.flipFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Square C)
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.toPowerSeriesAlg_apply : ∀ (R : Type u_2) [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : HahnSeries ℕ A), (HahnSeries.toPowerSeriesAlg R) f = PowerSeries.mk f.coeff
-- Aesop.Forward.Match
/-- Get the hypotheses from the match whose types are propositions.   -/
Aesop.ForwardRuleMatch.getPropHyps : Aesop.ForwardRuleMatch → Lean.MetaM (Array Lean.FVarId)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.X_eq_iff : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → (P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 ↔ P 0 / P 2 ^ 2 = Q 0 / Q 2 ^ 2)
-- Mathlib.Order.Comparable
IncompRel.refl : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Irrefl r] (a : α), IncompRel r a a
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that the slice formed by `startPos` and `endPos` contains is a match
of `pat` in `s` and it is longest among matches ending at `endPos`.
 -/
String.Slice.Pattern.Model.IsLongestRevMatchAt : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → s.Pos → Prop
-- Mathlib.RingTheory.Unramified.Field
Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable : ∀ (K : Type u_1) (L : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [Algebra.FormallyUnramified K L] [Algebra.EssFiniteType K L] [IsPurelyInseparable K L], (algebraMap K L).range = ⊤
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant monoid homomorphisms.  -/
«MulDistribMulActionHomLocal≺» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHomClass.instCoeToCoalgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {F : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : Module R A] →
              [inst_3 : AddCommMonoid B] →
                [inst_4 : Module R B] →
                  [inst_5 : CoalgebraStruct R A] →
                    [inst_6 : CoalgebraStruct R B] →
                      [inst_7 : FunLike F A B] → [CoalgHomClass F R A B] → CoeHead F (A →ₗc[R] B)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
/-- The composition-product of a measure and a kernel.  -/
MeasureTheory.Measure.compProd : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} → MeasureTheory.Measure α → ProbabilityTheory.Kernel α β → MeasureTheory.Measure (α × β)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) (x : Rˣ),
  (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : Nontrivial R}
  {inst_2 : StarRing R} {inst_3 : MetricSpace R} {inst_4 : IsTopologicalSemiring R} {inst_5 : ContinuousStar R}
  {inst_6 : NonUnitalRing A} {inst_7 : StarRing A} {inst_8 : TopologicalSpace A} {inst_9 : Module R A}
  {inst_10 : IsScalarTower R A A} {inst_11 : SMulCommClass R A A} [self : NonUnitalContinuousFunctionalCalculus R A p]
  (a : A), CompactSpace ↑(quasispectrum R a)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A local diffeomorphism is an open map.  -/
IsLocalDiffeomorph.isOpenMap : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N},
  IsLocalDiffeomorph I J n f → IsOpenMap f
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.deg_pow : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (n : ℕ), (c ^ n).deg = n • c.deg
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.instMonoid : {𝕜 : Type u_1} → [inst : SeminormedRing 𝕜] → [NormMulClass 𝕜] → [NormOneClass 𝕜] → Monoid ↑(Metric.sphere 0 1)
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.reApplyInnerSelf.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (x : E), T.reApplyInnerSelf x = RCLike.re (inner 𝕜 (T x) x)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.one : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] → [inst_1 : Monoid H] → {φ : (i : ι) → H →* G i} → One (Monoid.PushoutI φ)
-- Init.Data.RArray
/-- The crucial operation, written with very little abstractional overhead  -/
Lean.RArray.get : {α : Type u} → Lean.RArray α → ℕ → α
-- Lean.Meta.Tactic.Congr
_private.Lean.Meta.Tactic.Congr.0.Lean.MVarId.congrN.post : Bool → Lean.MVarId → StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_neg_one_X : ∀ {A : Type u_2} [inst : CommRing A], (PowerSeries.rescale (-1)) PowerSeries.X = -PowerSeries.X
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.add_assoc : ∀ {n : ℕ} (a b c : Fin n), a + b + c = a + (b + c)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.named : Lean.Name → Lean.Expr → Lean.Expr → Lean.Doc.ArgSpec✝
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_inv_naturality_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g ⟶ Z),
  CategoryTheory.CategoryStruct.comp η
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η)
        h)
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousOn.inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {f : α → G₀} {s : Set α} [inst_4 : TopologicalSpace α], ContinuousOn f s → (∀ x ∈ s, f x ≠ 0) → ContinuousOn f⁻¹ s
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.node : {α : Type} → Array α → Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Lean.Meta.DiscrTree.Trie α
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.induction_on' : ∀ {α : Type u} {motive : FreeAbelianGroup α → Prop} (z : FreeAbelianGroup α),
  motive 0 →
    (∀ (x : α), motive (pure x)) →
      (∀ (x : α), motive (Pure.pure x) → motive (-Pure.pure x)) →
        (∀ (x y : FreeAbelianGroup α), motive x → motive y → motive (x + y)) → motive z
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.analyticOnNhd : ∀ {𝕜 : 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 →L[𝕜] F)
  (s : Set E), AnalyticOnNhd 𝕜 (⇑f) s
-- Mathlib.MeasureTheory.Group.Arithmetic
List.measurable_fun_prod : ∀ {M : Type u_2} {α : Type u_3} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} (l : List (α → M)),
  (∀ f ∈ l, Measurable f) → Measurable fun x => (List.map (fun f => f x) l).prod
-- Init.Data.List.ToArray
List.rightpad_toArray : ∀ {α : Type u_1} (n : ℕ) (a : α) (l : List α), Array.rightpad n a l.toArray = (List.rightpad n a l).toArray
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.inter_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∩ t₂).Equiv (t₃ ∩ t₄)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.isCoprime_iff_gcd : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDedekindDomain A] {I J : Ideal A}, IsCoprime I J ↔ gcd I J = 1
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Cache.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} (rα : Option Q(CommRing «$α»))
  (dsα : Option Q(Semifield «$α»)) (czα : Option Q(CharZero «$α»)) (rα_1 : Option Q(CommRing «$α»))
  (dsα_1 : Option Q(Semifield «$α»)) (czα_1 : Option Q(CharZero «$α»)),
  ({ rα := rα, dsα := dsα, czα := czα } = { rα := rα_1, dsα := dsα_1, czα := czα_1 }) =
    (rα = rα_1 ∧ dsα = dsα_1 ∧ czα = czα_1)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α}
  {h' : k ∈ t.insertMany l} (contains : k ∈ t), (t.insertMany l).get k h' = t.get k contains
-- Mathlib.CategoryTheory.Sums.Basic
/-- The sum of two functors.  -/
CategoryTheory.Functor.sum : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                CategoryTheory.Functor A B → CategoryTheory.Functor C D → CategoryTheory.Functor (A ⊕ C) (B ⊕ D)
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_proj_comp : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  {φ : ι → Type i} [inst_3 : (i : ι) → AddCommMonoid (φ i)] [inst_4 : (i : ι) → Module R (φ i)]
  (f : M₂ →ₗ[R] (i : ι) → φ i), (LinearMap.pi fun x => LinearMap.proj x ∘ₗ f) = f
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.normBound_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L] {ι : Type u_3} (b : Module.Basis ι ℤ ↥L), 0 < ZLattice.normBound b
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.zero : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Zero Y], IsLocallyConstant 0
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.symm.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.symm = { toLinearEquiv := e.symm, norm_map' := ⋯ }
-- Init.Prelude
/-- Equality with `List.nil` is decidable even if the underlying type does not have decidable equality.
 -/
List.instDecidableEqNil : {α : Type u_1} → (a : List α) → Decidable (a = [])
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedState.restore : Lean.Elab.Term.SavedState → optParam Bool false → Lean.Elab.TermElabM Unit
-- Mathlib.Tactic.Linter.Whitespace
/-- A `FormatError` is the main structure tracking how some surface syntax differs from its
pretty-printed version.

In case of deviations, it contains the deviation's location within an ambient string.
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError : Type
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- `V(H)` denotes the `vertexSet` of a hypergraph `H`  -/
Hypergraph.«termV(_)» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_finprod : ∀ {α : Type u_1} {f : α → ℝ}, (∀ (a : α), 0 < f a) → Real.log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), Real.log (f a)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_inv : ∀ {S : Type u_5} [inst : Semifield S] [inst_1 : LinearOrder S] {R : Type u_6} [inst_2 : DivisionSemiring R]
  (abv : R → S) [IsAbsoluteValue abv] (a : R), abv a⁻¹ = (abv a)⁻¹
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stepAux.match_1.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ]
  (motive : Turing.TM1.Stmt Γ Λ σ → σ → Turing.Tape Γ → Sort u_4) (s : Γ → σ → σ) (q : Turing.TM1.Stmt Γ Λ σ) (v : σ)
  (T : Turing.Tape Γ)
  (h_1 :
    (d : Turing.Dir) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.move d q) v T)
  (h_2 :
    (a : Γ → σ → Γ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.write a q) v T)
  (h_3 :
    (s : Γ → σ → σ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.load s q) v T)
  (h_4 :
    (p : Γ → σ → Bool) →
      (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v T)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.goto l) v T)
  (h_6 : (v : σ) → (T : Turing.Tape Γ) → motive Turing.TM1.Stmt.halt v T),
  (match Turing.TM1.Stmt.load s q, v, T with
    | Turing.TM1.Stmt.move d q, v, T => h_1 d q v T
    | Turing.TM1.Stmt.write a q, v, T => h_2 a q v T
    | Turing.TM1.Stmt.load s q, v, T => h_3 s q v T
    | Turing.TM1.Stmt.branch p q₁ q₂, v, T => h_4 p q₁ q₂ v T
    | Turing.TM1.Stmt.goto l, v, T => h_5 l v T
    | Turing.TM1.Stmt.halt, v, T => h_6 v T) =
    h_3 s q v T
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.linearEquivFunOnFinite_symm_single : ∀ (R : Type u_9) (M : Type u_11) (α : Type u_12) [inst : Finite α] [inst_1 : AddCommMonoid M] [inst_2 : Semiring R]
  [inst_3 : Module R M] [inst_4 : DecidableEq α] (x : α) (m : M),
  (Finsupp.linearEquivFunOnFinite R M α).symm (Pi.single x m) = fun₀ | x => m
-- Lean.Data.KVMap
Lean.KVMap.mk.inj : ∀ {entries entries_1 : List (Lean.Name × Lean.DataValue)},
  { entries := entries } = { entries := entries_1 } → entries = entries_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyLE?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.getKeyLE? k t₁ = Std.DTreeMap.Internal.Impl.getKeyLE? k t₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {k fallback : α}, (cmp k (t.minKeyD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork hf hg c hc).right =
    CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftMonoidWithZeroHom_injective : ∀ {G₀ : Type u_1} {R : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : CommRing R] [Nontrivial R]
  (φ : Polynomial R →*₀ G₀) (hφ : Function.Injective ⇑φ)
  (hφ' : optParam (nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) ⋯),
  Function.Injective ⇑(RatFunc.liftMonoidWithZeroHom φ hφ')
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectSuccessorOf.trans : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it'' it' it : Std.IterM m β},
  it''.IsPlausibleIndirectSuccessorOf it' →
    it'.IsPlausibleIndirectSuccessorOf it → it''.IsPlausibleIndirectSuccessorOf it
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.auxEquiv_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (a : A) (b : B),
  (GradedTensorProduct.auxEquiv R 𝒜 ℬ) (a ᵍ⊗ₜ[R] b) = (DirectSum.decompose 𝒜) a ⊗ₜ[R] (DirectSum.decompose ℬ) b
-- Mathlib.Data.Rat.Lemmas
Rat.inv_intCast_num : ∀ (a : ℤ), (↑a)⁻¹.num = a.sign