mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv : ∀ {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.δToCycles_cyclesIso_inv._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv._auto_3),
  CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv =
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.diagram.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : SizeOf J] {j k : J} (f : j ⟶ k),
  sizeOf (CategoryTheory.BiconeHom.diagram f) = 1 + sizeOf j + sizeOf k + sizeOf f
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqPower.beq.match_1.splitter : (motive : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Power → Sort u_1) →
  (x x_1 : Lean.Grind.CommRing.Power) →
    ((a : Lean.Grind.CommRing.Var) →
        (a_1 : ℕ) → (b : Lean.Grind.CommRing.Var) → (b_1 : ℕ) → motive { x := a, k := a_1 } { x := b, k := b_1 }) →
      ((x x_2 : Lean.Grind.CommRing.Power) →
          (∀ (a : Lean.Grind.CommRing.Var) (a_1 : ℕ) (b : Lean.Grind.CommRing.Var) (b_1 : ℕ),
              x = { x := a, k := a_1 } → x_2 = { x := b, k := b_1 } → False) →
            motive x x_2) →
        motive x x_1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.id.toOplax : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C),
  (CategoryTheory.Oplax.StrongTrans.id F).toOplax = CategoryTheory.Oplax.OplaxTrans.id F
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.isPreconnected_setOfPred_wOppSide`. -/
AffineSubspace.isPreconnected_setOf_wOppSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P),
  IsPreconnected {y | s.WOppSide x y}
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv_symm_C_X : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (c : S₂),
  (MvPolynomial.sumAlgEquiv R S₁ S₂).symm (MvPolynomial.C (MvPolynomial.X c)) = MvPolynomial.X (Sum.inr c)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
is a neighborhood of the preimage.  -/
extChartAt_preimage_mem_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {t : Set M} [inst_5 : ChartedSpace H M] {x : M},
  t ∈ nhds x → ↑(extChartAt I x).symm ⁻¹' t ∈ nhds (↑(extChartAt I x) x)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl : Lean.Compiler.LCNF.Purity → Type
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.id_comp : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  (f : X →ₑ[φ] Y), (MulActionHom.id N).comp f = f
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.bot_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X), ⊥.arrows f ↔ False
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (self : CategoryTheory.CommGrp C), CategoryTheory.IsCommMonObj self.X
-- Mathlib.Algebra.Module.End
IsAddUnit.smul_right : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} (x : M),
  IsAddUnit r → IsAddUnit (r • x)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsSwap.orderOf : ∀ {α : Type u_1} [inst : DecidableEq α] [Finite α] {σ : Equiv.Perm α}, σ.IsSwap → orderOf σ = 2
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesEntry.mk.sizeOf_spec : ∀ (declName : Lean.Name) (eager : Bool),
  sizeOf { declName := declName, eager := eager } = 1 + sizeOf declName + sizeOf eager
-- Init.Data.Int.DivMod.Basic
Int.negSucc_ediv_negSucc : ∀ {a b : ℕ}, Int.negSucc a / Int.negSucc b = ↑(a / (b + 1) + 1)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.pre_pre : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)] {L : Type u₃} [inst_5 : CategoryTheory.Category.{v₃, u₃} L]
  (D : CategoryTheory.Functor L K) [h : CategoryTheory.Limits.HasLimit (D.comp (E.comp F))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre F E)
      (CategoryTheory.Limits.limit.pre (E.comp F) D) =
    CategoryTheory.Limits.limit.pre F (D.comp E)
-- Mathlib.Analysis.Normed.Operator.Conformal
IsConformalMap.comp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {G : Type u_4} [inst : NormedField R] [inst_1 : SeminormedAddCommGroup M]
  [inst_2 : SeminormedAddCommGroup N] [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace R M]
  [inst_5 : NormedSpace R N] [inst_6 : NormedSpace R G] {f : M →L[R] N} {g : N →L[R] G},
  IsConformalMap g → IsConformalMap f → IsConformalMap (g ∘SL f)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.mk.injEq : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (toFun : G → E) (rightInverse_rightHom : Function.RightInverse toFun ⇑S.rightHom)
  (toFun_1 : G → E) (rightInverse_rightHom_1 : Function.RightInverse toFun_1 ⇑S.rightHom),
  ({ toFun := toFun, rightInverse_rightHom := rightInverse_rightHom } =
      { toFun := toFun_1, rightInverse_rightHom := rightInverse_rightHom_1 }) =
    (toFun = toFun_1)
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p], Finsupp.filter p 0 = 0
-- Init.Control.Lawful.Instances
OptionT.run_liftWith : ∀ {m : Type u → Type u_1} {α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m α), (liftWith f).run = some <$> f fun {β} x => x.run
-- Init.Data.UInt.Lemmas
UInt8.toNat_add : ∀ (a b : UInt8), (a + b).toNat = (a.toNat + b.toNat) % 2 ^ 8
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.subFn? : Lean.Meta.Grind.Arith.CommRing.Ring → Option Lean.Expr
-- Mathlib.Data.Real.Embedding
Archimedean.embedRealFun_strictMono : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M], StrictMono Archimedean.embedRealFun
-- Mathlib.Algebra.Group.Units.Defs
Units.val_one : ∀ {α : Type u} [inst : Monoid α], ↑1 = 1
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.isBigO_log_mul_const_log_atTop : ∀ (c : ℝ), (fun x => Real.log (x * c)) =O[Filter.atTop] Real.log
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- A subgroup is either the trivial subgroup or contains a nonzero element.  -/
AddSubgroup.bot_or_exists_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H = ⊥ ∨ ∃ x ∈ H, x ≠ 0
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.below.imp : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {motive : (a : L.BoundedFormula α n) → a.IsQF → Prop}
  {φ₁ φ₂ : L.BoundedFormula α n} (h₁ : φ₁.IsQF) (h₂ : φ₂.IsQF),
  FirstOrder.Language.BoundedFormula.IsQF.below h₁ →
    motive φ₁ h₁ →
      FirstOrder.Language.BoundedFormula.IsQF.below h₂ → motive φ₂ h₂ → FirstOrder.Language.BoundedFormula.IsQF.below ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isNone_minKey?_eq_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey?.isNone = t.isEmpty
-- Init.Data.Array.Zip
Array.zipWith_map : ∀ {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} {f : γ → δ → μ} {g : α → γ} {h : β → δ}
  {as : Array α} {bs : Array β},
  Array.zipWith f (Array.map g as) (Array.map h bs) = Array.zipWith (fun a b => f (g a) (h b)) as bs
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- Radii of the balls  -/
Besicovitch.BallPackage.r : {β : Type u_1} → {α : Type u_2} → Besicovitch.BallPackage β α → β → ℝ
-- Mathlib.Analysis.Calculus.Deriv.Comp
/-- The chain rule.

Note that the function `h₂` is a function on an algebra. If you are looking for the chain rule
with `h₂` taking values in a vector space, use `HasDerivAt.scomp_of_eq`.  -/
HasDerivAt.comp_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' y : 𝕜'},
  HasDerivAt h₂ h₂' y → HasDerivAt h h' x → y = h x → HasDerivAt (h₂ ∘ h) (h₂' * h') x
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsInitial.isVanKampenColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {X : C}
  (h : CategoryTheory.Limits.IsInitial X), CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.asEmptyCocone X)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateCol_add_smul_self : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  {i j : n}, i ≠ j → ∀ (c : R), (A.updateCol i fun k => A k i + c • A k j).det = A.det
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If `f` has a Taylor series up to `n`, then it is `C^n`.  -/
HasFTaylorSeriesUpTo.contDiff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : ℕ∞} {f' : E → FormalMultilinearSeries 𝕜 E F}, HasFTaylorSeriesUpTo (↑n) f f' → ContDiff 𝕜 (↑n) f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.associator_hom_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F₁ F₂ F₃ : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.MonoidalCategoryStruct.associator F₁ F₂ F₃).hom.app j =
    (CategoryTheory.MonoidalCategoryStruct.associator (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.shift_map_op : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] {X Y : C} (f : X ⟶ Y)
  (n : ℤ),
  (CategoryTheory.shiftFunctor Dᵒᵖ n).map (F.map f).op =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F.op n).inv.app (Opposite.op Y))
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f.op).unop).op
        ((CategoryTheory.Functor.commShiftIso F.op n).hom.app (Opposite.op X)))
-- Mathlib.Algebra.Group.Defs
AddLeftCancelSemigroup.ext : ∀ {G : Type u} {x y : AddLeftCancelSemigroup G}, Add.add = Add.add → x = y
-- Mathlib.Order.Filter.Bases.Finite
Pairwise.exists_mem_filter_basis_of_disjoint : ∀ {α : Type u_1} {I : Type u_7} [Finite I] {l : I → Filter α} {ι : I → Sort u_6} {p : (i : I) → ι i → Prop}
  {s : (i : I) → ι i → Set α},
  Pairwise (Function.onFun Disjoint l) →
    (∀ (i : I), (l i).HasBasis (p i) (s i)) →
      ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Function.onFun Disjoint fun i => s i (ind i))
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.mkSol_injective : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R), Function.Injective E.mkSol
-- Init.Grind.Norm
Lean.Grind.zero_sub : ∀ (a : ℕ), 0 - a = 0
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- A positive linear map is a linear map that is also an order homomorphism.  -/
PositiveLinearMap : (R : Type u_1) →
  (E₁ : Type u_2) →
    (E₂ : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] → [PartialOrder E₂] → [Module R E₁] → [Module R E₂] → Type (max u_2 u_3)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).isEmpty = ((m.isEmpty || m.size == 1 && m.contains k) && (f (m.get? k)).isNone)
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.findLeadingSpacesSize.findNextLine.eq_def : ∀ {s : String} (it : s.Pos) (min : ℕ),
  String.findLeadingSpacesSize.findNextLine✝ it min =
    if h : it.IsAtEnd then min
    else
      if (it.get h == '\n') = true then String.findLeadingSpacesSize.consumeSpaces✝ (it.next h) 0 min
      else String.findLeadingSpacesSize.findNextLine✝ (it.next h) min
-- Lean.Meta.Check
_private.Lean.Meta.Check.0.Lean.Meta.checkAux : Lean.Expr → Lean.MetaM Unit
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- `Completion.toCompletion` as a ring isomorphism onto the underlying completion.  -/
NumberField.InfinitePlace.Completion.equiv : {K : Type u_1} → [inst : Field K] → (v : NumberField.InfinitePlace K) → v.Completion ≃+* (↑v).Completion
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toRingEquiv : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A ≃ₐ[R] B) → A ≃+* B
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_eq_fold : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (s : Finset ι) (f : ι → M),
  ∏ i ∈ s, f i = Finset.fold (fun x1 x2 => x1 * x2) 1 f s
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.takeUntil : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} {p : G.Walk v w},
  p.IsTrail → ∀ (h : u ∈ p.support), (p.takeUntil u h).IsTrail
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instHashablePosition : Hashable Lean.Lsp.Position
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.id_comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f),
  ProbabilityTheory.Kernel.id.comap f hf = ProbabilityTheory.Kernel.deterministic f hf
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The distance is induced by the norm.  -/
SeminormedRing.dist_eq : ∀ {α : Type u_5} [self : SeminormedRing α] (x y : α), dist x y = ‖-x + y‖
-- Init.Data.UInt.Bitwise
UInt8.zero_or : ∀ {a : UInt8}, 0 ||| a = a
-- Mathlib.Tactic.IntervalCases
/-- The new subgoal, of the form `⊢ x = rhs → tgt`  -/
Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal.goal : Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal → Lean.MVarId
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toOplaxFunctor_map : ∀ {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)
  {X Y : CategoryTheory.LocallyDiscrete C} (x : X ⟶ Y),
  F.toOplaxFunctor.map x =
    match x with
    | { as := f } => (F.map f).toLoc
-- Mathlib.Algebra.Group.UniqueProds.Basic
uniqueAdd_of_twoUniqueAdd : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G},
  (1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueAdd A B p1.1 p1.2 ∧ UniqueAdd A B p2.1 p2.2) →
    A.Nonempty → B.Nonempty → ∃ a ∈ A, ∃ b ∈ B, UniqueAdd A B a b
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.mk : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                {P : RootPairing ι R M N} →
                                  {Q : RootPairing ι₂ R M₂ N₂} →
                                    (toHom : P.Hom Q) →
                                      Function.Bijective ⇑toHom.weightMap →
                                        Function.Bijective ⇑toHom.coweightMap → P.Equiv Q
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.fst_comp_inr : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  (AddMonoidHom.fst M N).comp (AddMonoidHom.inr M N) = 0
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
CategoryTheory.Limits.PushoutCocone.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl inl_1 : Y ⟶ W)
  (e_inl : inl = inl_1) (inr inr_1 : Z ⟶ W) (e_inr : inr = inr_1)
  (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr),
  CategoryTheory.Limits.PushoutCocone.mk inl inr eq = CategoryTheory.Limits.PushoutCocone.mk inl_1 inr_1 ⋯
-- Mathlib.Tactic.Translate.Core
/-- Combine two known `RelevantArg`s by taking the smallest value of the two.
Recall that if there are multiple relevant arguments, `relevant_arg` is set to the smallest one.  -/
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.RelevantArg.min : Mathlib.Tactic.Translate.RelevantArg → Mathlib.Tactic.Translate.RelevantArg → Mathlib.Tactic.Translate.RelevantArg
-- Mathlib.Data.Sym.Basic
Sym.cons_swap : ∀ {α : Type u_1} {n : ℕ} (a b : α) (s : Sym α n), a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s
-- Mathlib.Algebra.Module.Submodule.Invariant
LinearEquiv.map_mem_invtSubmodule_iff : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {f : Module.End R N} {e : M ≃ₗ[R] N} {p : Submodule R M},
  Submodule.map (↑e) p ∈ f.invtSubmodule ↔ p ∈ (e.symm.conj f).invtSubmodule
-- Lean.Elab.DeclModifiers
Lean.Elab.instToStringVisibility : ToString Lean.Elab.Visibility
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
GaloisConnection.cof_le_lift : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : β → α} {g : α → β},
  GaloisConnection f g → Cardinal.lift.{u, v} (Order.cof β) ≤ Cardinal.lift.{v, u} (Order.cof α)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.ExtDTreeMap.Const.minEntry! : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtDTreeMap α (fun x => β) cmp → α × β
-- Mathlib.Data.Finset.Insert
Finset.cons_subset : ∀ {α : Type u_1} {s t : Finset α} {a : α} {h : a ∉ s}, Finset.cons a s h ⊆ t ↔ a ∈ t ∧ s ⊆ t
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.isIdempotentElem_projection`.

---

The linear projection onto a subspace along its complement is an idempotent.  -/
Submodule.IsCompl.projection_isIdempotentElem : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), IsIdempotentElem (p.projection q hpq)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableOn.cpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {c : ℂ},
  DifferentiableOn ℂ f s → (∀ x ∈ s, f x ∈ Complex.slitPlane) → DifferentiableOn ℂ (fun x => f x ^ c) s
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- Refinement of `IsPreconnected.constant` only assuming the map factors through a
discrete subset of the target.  -/
IsPreconnected.constant_of_mapsTo : ∀ {α : Type u} [inst : TopologicalSpace α] {S : Set α},
  IsPreconnected S →
    ∀ {β : Type u_3} [inst_1 : TopologicalSpace β] {T : Set β},
      IsDiscrete T → ∀ {f : α → β}, ContinuousOn f S → Set.MapsTo f S T → ∀ {x y : α}, x ∈ S → y ∈ S → f x = f y
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] [Nonempty D],
  (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding F).Faithful
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj}
  {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} (s t : c₁.pt ⟶ c₂.pt)
  (hs :
    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
      CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) =
        CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd))
  (ht :
    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
      CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 })
  (i : CategoryTheory.Limits.Fork s t),
  (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i).pt = i.pt
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- `invertibleOfFromBlocksZero₂₁Invertible` and `Matrix.fromBlocksZero₂₁Invertible` form
an equivalence.  -/
Matrix.fromBlocksZero₂₁InvertibleEquiv : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (D : Matrix n n α) → Invertible (Matrix.fromBlocks A B 0 D) ≃ Invertible A × Invertible D
-- Mathlib.Analysis.Complex.Hadamard
/-- A bound to the norm of `f` on the line `z.re = l` induces a bound to the norm of
`scale f l u z` on the line `z.re = 0`.  -/
Complex.HadamardThreeLines.scale_bound_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {l u a : ℝ},
  (∀ z ∈ Complex.re ⁻¹' {l}, ‖f z‖ ≤ a) → ∀ z ∈ Complex.re ⁻¹' {0}, ‖Complex.HadamardThreeLines.scale f l u z‖ ≤ a
-- Init.Data.Order.Factories
/-- This lemma characterizes in terms of `LT α` when a `Max α` instance
"behaves like an supremum operator" with respect to `LE.ofLT α`.
 -/
Std.LawfulOrderSup.of_lt : ∀ {α : Type u} [inst : Max α] [inst_1 : LT α], (∀ (a b c : α), c < a ⊔ b ↔ c < a ∨ c < b) → Std.LawfulOrderSup α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensParams.mk.injEq : ∀ (textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier),
  ({ textDocument := textDocument } = { textDocument := textDocument_1 }) = (textDocument = textDocument_1)