mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.preimage_ball : ∀ {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₂) (x : E₂) (r : ℝ), ⇑e ⁻¹' Metric.ball x r = Metric.ball (e.symm x) r
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.multispanMapIso.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MultispanShape} (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) (a : J.L)
  (h_1 : (a : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left a))
  (h_2 : (a : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right a)),
  (match CategoryTheory.Limits.WalkingMultispan.left a with
    | CategoryTheory.Limits.WalkingMultispan.left a => h_1 a
    | CategoryTheory.Limits.WalkingMultispan.right a => h_2 a) =
    h_1 a
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_2.go : {motive_1 : Lean.Elab.InfoTree → Sort u} →
  {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u} →
    {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} →
      {motive_4 : Array Lean.Elab.InfoTree → Sort u} →
        {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
          {motive_6 : List Lean.Elab.InfoTree → Sort u} →
            {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
              (t : Lean.PersistentArrayNode Lean.Elab.InfoTree) →
                ((t : Lean.Elab.InfoTree) → t.below → motive_1 t) →
                  ((t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t) →
                    ((t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t) →
                      ((t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t) →
                        ((t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                            Lean.Elab.InfoTree.below_4 t → motive_5 t) →
                          ((t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t) →
                            ((t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                                Lean.Elab.InfoTree.below_6 t → motive_7 t) →
                              motive_3 t ×' Lean.Elab.InfoTree.below_2 t
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
/-- In the category of simplicial sets, a strong anodyne extension is a morphism
which belongs to the closure of horn inclusions by pushouts, coproducts,
transfinite compositions (but not by retracts). We define this class here
by saying that `f : X ⟶ Y` is a strong anodyne extension if `f` is a monomorphism
and there exists a regular pairing (in the sense of Moss) for the subcomplex
`Subcomplex.range f` of `Y`.  -/
SSet.strongAnodyneExtensions : CategoryTheory.MorphismProperty SSet
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNNNorm_def : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A‖₊ = Finset.univ.sup fun i => ∑ j, ‖A i j‖₊
-- Mathlib.Algebra.Group.End
AddAut.apply_neg_self : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M) (m : M), e ((-e) m) = m
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.structuredArrow_iso_iff : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {T : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} T] (P : CategoryTheory.MorphismProperty T) [P.RespectsIso]
  {L : CategoryTheory.Functor A T} {X : T} {f g : CategoryTheory.StructuredArrow X L} (e : f ≅ g), P f.hom ↔ P g.hom
-- Mathlib.Geometry.Manifold.Immersion
/-- A `C^n` immersion at `x` is `C^n` at `x`.  -/
Manifold.IsImmersionAtOfComplement.contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsImmersionAtOfComplement F I J n f x → ContMDiffAt I J n f x
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_top_left_le_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ⁅⊤, H⁆ ≤ H ↔ H.Normal
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.hasCoeT : {R : Type u_1} → [inst : CommRing R] → {f : Polynomial R} → CoeTC R (AdjoinRoot f)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.modify.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (f : β a → β a),
  Std.DHashMap.Internal.AssocList.modify a f Std.DHashMap.Internal.AssocList.nil = Std.DHashMap.Internal.AssocList.nil
-- Mathlib.Data.Multiset.Count
Multiset.count_singleton_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Multiset.count a {a} = 1
-- Mathlib.Tactic.TermCongr
/-- Returns the proof that `lhs ≍ rhs`. Fails if the `CongrResult` is inapplicable.
If `pf? = none`, this returns the `rfl` proof.  -/
Mathlib.Tactic.TermCongr.CongrResult.heq : Mathlib.Tactic.TermCongr.CongrResult → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_param_mul_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    (Asymptotics.SuperpolynomialDecay l k (k * f) ↔ Asymptotics.SuperpolynomialDecay l k f)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcOptions.highlightMatchesProvider? : Lean.Lsp.RpcOptions → Option Lean.Lsp.HighlightMatchesOptions
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ}
  {k : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filterMap f m).getKey? k =
    (m.getKey? k).pfilter fun x h' => (f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)).isSome
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n m : ℕ}
  (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (F : CategoryTheory.ComposableArrows C m) {X Y : Fin (n + 1)}
  (f : X ⟶ Y), ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).obj F).map f = F.map (Φ.map f)
-- Mathlib.Analysis.CStarAlgebra.Basic
instCStarRingReal : CStarRing ℝ
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_image_of_injOn : ∀ {α : Type u_3} {β : Type u_4} {f : α → β} {s : Set α}, Set.InjOn f s → ENat.card ↑(f '' s) = ENat.card ↑s
-- Mathlib.GroupTheory.Archimedean
/-- Given a subgroup `H` of a decidable linearly ordered
archimedean abelian group `G`, if there exists a minimal element `a` of `H ∩ G_{>0}` then `H` is
generated by `a`.  -/
AddSubgroup.cyclic_of_min : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
  {H : AddSubgroup G} {a : G}, IsLeast {g | g ∈ H ∧ 0 < g} a → H = AddSubgroup.closure {a}
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.nonUnitalSubringClass : ∀ (S : Type u_1) (R : Type u) [inst : SetLike S R] [inst_1 : NonAssocRing R] [SubringClass S R],
  NonUnitalSubringClass S R
-- Init.Data.Array.Lemmas
List.all_toArray : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.toArray.all p = l.all p
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_snd_eq_insertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α)
  (b : β a),
  (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew a b t htb).2 = Std.DTreeMap.Internal.Impl.insertIfNew a b t htb
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.comp₃ : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_6}
  {E₂ : Type u_7} {E₃ : Type u_8} [inst_5 : NormedAddCommGroup E₁] [inst_6 : NormedAddCommGroup E₂]
  [inst_7 : NormedAddCommGroup E₃] [inst_8 : NormedSpace 𝕜 E₁] [inst_9 : NormedSpace 𝕜 E₂] [inst_10 : NormedSpace 𝕜 E₃]
  {g : E₁ × E₂ × E₃ → G} {f₁ : F → E₁} {f₂ : F → E₂} {f₃ : F → E₃},
  ContDiff 𝕜 n g → ContDiff 𝕜 n f₁ → ContDiff 𝕜 n f₂ → ContDiff 𝕜 n f₃ → ContDiff 𝕜 n fun x => g (f₁ x, f₂ x, f₃ x)
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.rightUnitor_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Arrow C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Arrow C)))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (t.erase k).maxKey he = t.maxKey ⋯ ↔ ¬cmp k (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.forall_rel_cons_ext : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a : α} {r : ⦃a : α⦄ → δ a → δ a → Prop}
  {b₁ b₂ : δ a} {f₁ f₂ : (a' : α) → a' ∈ m → δ a'},
  r b₁ b₂ →
    (∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)) →
      ∀ (a_1 : α) (ha : a_1 ∈ a ::ₘ m), r (Multiset.Pi.cons m a b₁ f₁ a_1 ha) (Multiset.Pi.cons m a b₂ f₂ a_1 ha)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
/-- The balanced core of `t` is maximal in the sense that it contains any balanced subset
`s` of `t`.  -/
Balanced.subset_balancedCore_of_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s t : Set E},
  Balanced 𝕜 s → s ⊆ t → s ⊆ balancedCore 𝕜 t
-- Mathlib.Topology.Homotopy.Path
/-- The type of homotopies between two paths.
 -/
Path.Homotopy : {X : Type u} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → Path x₀ x₁ → Path x₀ x₁ → Type (max 0 u)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.LocallyOfFiniteType f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_swap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f)
      (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id B)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id A))
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id Y) f)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad n Pred EPred] [inst_10 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_12 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ}
  {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let __x ← f b
          match __x with
            | some c => pure (g d c)
            | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.filterMapM f it) ⦃ Q; eQ ⦄
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.mk.sizeOf_spec : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (map : SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
  (δ_castSucc_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.castSucc) map = f.map)
      SSet.PtSimplex.RelStruct.δ_castSucc_map._autoParam)
  (δ_succ_map :
    autoParam (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) map = g.map)
      SSet.PtSimplex.RelStruct.δ_succ_map._autoParam)
  (δ_map_of_lt :
    autoParam (∀ j < i.castSucc, CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_lt._autoParam)
  (δ_map_of_gt :
    autoParam
      (∀ (j : Fin (n + 2)), i.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) map = SSet.const x)
      SSet.PtSimplex.RelStruct.δ_map_of_gt._autoParam),
  sizeOf
      { map := map, δ_castSucc_map := δ_castSucc_map, δ_succ_map := δ_succ_map, δ_map_of_lt := δ_map_of_lt,
        δ_map_of_gt := δ_map_of_gt } =
    1 + sizeOf map + sizeOf δ_castSucc_map + sizeOf δ_succ_map
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.exists_structureMap_eq_of_forall : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι}
  {x : RestrictedProduct (fun i => R i) (fun i => A i) 𝓕},
  (∀ (i : ι), ↑x i ∈ A i) → ∃ x', RestrictedProduct.structureMap R A 𝓕 x' = x
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.ι₃_desc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  CategoryTheory.CategoryStruct.comp SSet.horn₃₁.ι₃ (SSet.horn₃₁.desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) = f₃
-- Mathlib.Topology.EMetricSpace.Defs
AddOpposite.edist_unop : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y : αᵃᵒᵖ), edist (AddOpposite.unop x) (AddOpposite.unop y) = edist x y
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} {I J : Ideal S} [I.IsPrime],
  I ≤ J →
    ∀ {r : S},
      r ∈ ↑J \ ↑I →
        ∀ {p : Polynomial R},
          Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0 →
            Polynomial.eval₂ f r p ∈ I → ∃ i, p.coeff i ∈ ↑(Ideal.comap f J) \ ↑(Ideal.comap f I)
-- Mathlib.RingTheory.PrincipalIdealDomain
PrincipalIdealRing.ne_zero_of_mem_factors : ∀ {R : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] {a b : R},
  a ≠ 0 → b ∈ PrincipalIdealRing.factors a → b ≠ 0
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ : I₂),
  (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).X i₂ = (F.obj (K₁.X i₁)).obj (K₂.X i₂)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_zero : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α 0) (p : (j : Fin n) → α (Fin.succAbove 0 j)),
  Fin.insertNth 0 x p = Fin.cons x fun j => cast ⋯ (p j)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.collectCtors : Lean.Meta.Match.Problem → Array Lean.Name
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essImage.liftFunctorCompIso_inv_app : ∀ {J : Type u_1} {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [inst_3 : F.Full] [inst_4 : F.Faithful]
  (hG : ∀ (j : J), F.essImage (G.obj j)) (X : J),
  (CategoryTheory.Functor.essImage.liftFunctorCompIso G F hG).inv.app X =
    (F.toEssImage.objObjPreimageIso { obj := G.obj X, property := ⋯ }).inv.hom
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.id_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x x_1 : C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Functor.id C) x x_1 =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Functor.id C).obj x)
        ((CategoryTheory.Functor.id C).obj x_1))
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- If f : G → H is a multiplicative homomorphism between two monoids and
`∀ (a : G) (x : k), a • x = (f a) • x`, then `mapDomain f` is a ring homomorphism
between their skew monoid algebras.  -/
SkewMonoidAlgebra.mapDomainRingHom : {α : Type u_3} →
  {α₂ : Type u_4} →
    {β : Type u_5} →
      {F : Type u_6} →
        [inst : Semiring β] →
          [inst_1 : Monoid α] →
            [inst_2 : Monoid α₂] →
              [inst_3 : FunLike F α α₂] →
                [inst_4 : MulSemiringAction α β] →
                  [inst_5 : MulSemiringAction α₂ β] →
                    [MonoidHomClass F α α₂] →
                      {f : F} → (∀ (a : α) (x : β), a • x = f a • x) → SkewMonoidAlgebra β α →+* SkewMonoidAlgebra β α₂
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_closure_pair : ∀ {C : Type u_2} [inst : CommGroup C] {x y z : C}, z ∈ Subgroup.closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z
-- Mathlib.RingTheory.DividedPowers.Padic
_private.Mathlib.RingTheory.DividedPowers.Padic.0.PadicInt.dpow'_norm_le_of_ne_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ},
  n ≠ 0 → ∀ {x : ℤ_[p]}, x ∈ Ideal.span {↑p} → ‖PadicInt.dpow'✝ p n ↑x‖ ≤ (↑p)⁻¹
-- Mathlib.Analysis.Complex.Norm
Complex.sq_norm_sub_sq_re : ∀ (z : ℂ), ‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.instInhabitedWalkingParallelFamily : {a : Type u_1} → Inhabited (CategoryTheory.Limits.WalkingParallelFamily a)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- A version of `NonUnitalAlgHom.quasispectrum_apply_subset` which allows for `quasispectrum R`,
where `R` is a *semi*ring, but `φ` must still function over a scalar ring `S`. In this case, we
need `S` to be explicit. The primary use case is, for instance, `R := ℝ≥0` and `S := ℝ` or
`S := ℂ`.  -/
NonUnitalAlgHom.quasispectrum_apply_subset' : ∀ {F : Type u_3} {R : Type u_4} (S : Type u_5) {A : Type u_6} {B : Type u_7} [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : NonUnitalRing A] [inst_3 : NonUnitalRing B] [inst_4 : Module R S]
  [inst_5 : Module S A] [inst_6 : Module R A] [inst_7 : Module S B] [inst_8 : Module R B] [IsScalarTower R S A]
  [IsScalarTower R S B] [inst_11 : FunLike F A B] [NonUnitalAlgHomClass F S A B] (φ : F) (a : A),
  quasispectrum R (φ a) ⊆ quasispectrum R a
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.compMultilinearMapₗ_apply : ∀ {R : Type uR} (S : Type uS) {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂]
  [inst_8 : AddCommMonoid M₃] [inst_9 : Module S M₃] [inst_10 : Module R M₃] [inst_11 : SMulCommClass R S M₃]
  [inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂),
  (LinearMap.compMultilinearMapₗ S g) f = g.compMultilinearMap f
-- Mathlib.Topology.Algebra.Module.Complement
/-- Given continuous linear maps `φ : p →L[R] F` and `ψ : q →L[R] F` from topological complement
submodules `p` and `q` of `E`, `ContinuousLinearMap.ofIsCompl` is the induced continuous linear map
`E →L[R] F` over the entire module.

This is the continuous version of `LinearMap.ofIsCompl`.  -/
ContinuousLinearMap.ofIsTopCompl : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      {F : Type u_3} →
        [inst_1 : TopologicalSpace E] →
          [inst_2 : AddCommGroup E] →
            [inst_3 : Module R E] →
              [IsTopologicalAddGroup E] →
                [inst_5 : TopologicalSpace F] →
                  [inst_6 : AddCommGroup F] →
                    [inst_7 : Module R F] →
                      [ContinuousAdd F] →
                        {p q : Submodule R E} → Submodule.IsTopCompl p q → (↥p →L[R] F) → (↥q →L[R] F) → E →L[R] F
-- Mathlib.Topology.Path
/-- Any function `φ : Π (a : α), Path (x a) (y a)` can be seen as a function `α × I → X`.  -/
Path.instHasUncurryPath : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {α : Type u_4} → {x y : α → X} → Function.HasUncurry ((a : α) → Path (x a) (y a)) (α × ↑unitInterval) X
-- Mathlib.Geometry.Euclidean.PerpBisector
/-- A point `c` belongs the perpendicular bisector of `[p₁, p₂]` iff `c -ᵥ midpoint ℝ p₁ p₂` is
orthogonal to `p₂ -ᵥ p₁`.  -/
AffineSubspace.mem_perpBisector_iff_inner_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c p₁ p₂ : P},
  c ∈ AffineSubspace.perpBisector p₁ p₂ ↔ inner ℝ (c -ᵥ midpoint ℝ p₁ p₂) (p₂ -ᵥ p₁) = 0
-- Lean.Meta.Tactic.Cases
Lean.Meta.getInductiveUniverseAndParams : Lean.Expr → Lean.MetaM (List Lean.Level × Array Lean.Expr)
-- Mathlib.Condensed.Discrete.Characterization
CondensedMod.instHasLimitsOfSizeModuleCat : ∀ (R : Type (u + 1)) [inst : Ring R], CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (ModuleCat R)
-- Aesop.Forward.LevelIndex
Aesop.instDecidableEqLevelIndex.decEq : (x x_1 : Aesop.LevelIndex) → Decidable (x = x_1)
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.instInv.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : One M] [inst_1 : InvOneClass N],
  OneHom.instInv = { inv := fun f => { toFun := fun m => (f m)⁻¹, map_one' := ⋯ } }
-- Mathlib.Logic.Equiv.PartialEquiv
/-- If two partial equivs are equivalent, so are their inverses.  -/
PartialEquiv.EqOnSource.symm' : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → e.symm ≈ e'.symm