mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
_private.Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv.0.auxIsometry.congr_simp : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] [inst_4 : NormedAddCommGroup W]
  [inst_5 : InnerProductSpace 𝕜 W] [inst_6 : CompleteSpace W] (e e_1 : V ≃L[𝕜] W) (e_e : e = e_1) {α α_1 : 𝕜}
  (e_α : α = α_1) {α' α'_1 : 𝕜} (e_α' : α' = α'_1) (hα : α ≠ 0) (hα2 : α' * α' = α⁻¹)
  (he : ContinuousLinearMap.adjoint ↑e ∘SL ↑e = α • ContinuousLinearMap.id 𝕜 V)
  (he' : ↑e ∘SL ContinuousLinearMap.adjoint ↑e = α • ContinuousLinearMap.id 𝕜 W) (hαa : (starRingEnd 𝕜) α' = α'),
  auxIsometry✝ e hα hα2 he he' hαa = auxIsometry✝ e_1 ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
summable_sum_mul_antidiagonal_of_summable_mul : ∀ {α : Type u_3} {A : Type u_4} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A]
  [inst_2 : TopologicalSpace α] [inst_3 : NonUnitalNonAssocSemiring α] {f g : A → α} [T3Space α]
  [IsTopologicalSemiring α],
  (Summable fun x => f x.1 * g x.2) → Summable fun n => ∑ kl ∈ Finset.HasAntidiagonal.antidiagonal n, f kl.1 * g kl.2
-- Mathlib.Data.Prod.TProd
_private.Mathlib.Data.Prod.TProd.0.List.TProd.mk.match_1.eq_2 : ∀ {ι : Type u_1} (motive : List ι → Sort u_2) (i : ι) (is : List ι) (h_1 : Unit → motive [])
  (h_2 : (i : ι) → (is : List ι) → motive (i :: is)),
  (match i :: is with
    | [] => h_1 ()
    | i :: is => h_2 i is) =
    h_2 i is
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.completeMultipartiteGraph.colorable_of_cliqueFree : ∀ {n : ℕ} {ι : Type u_4} (V : ι → Type u_5) (f : (i : ι) → V i),
  (SimpleGraph.completeMultipartiteGraph V).CliqueFree n → (SimpleGraph.completeMultipartiteGraph V).Colorable (n - 1)
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecomposition_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  (o : CategoryTheory.HomOrthogonal s) {α β : Type} [inst_3 : Finite α] [inst_4 : Finite β] {f : α → ι} {g : β → ι}
  (z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))),
  o.matrixDecomposition.symm z =
    CategoryTheory.Limits.biproduct.matrix fun j k =>
      if h : f j = g k then CategoryTheory.CategoryStruct.comp (z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩) (CategoryTheory.eqToHom ⋯) else 0
-- Mathlib.RingTheory.IsAdjoinRoot
AdjoinRoot.isAdjoinRoot.eq_1 : ∀ {R : Type u} [inst : CommRing R] (f : Polynomial R),
  AdjoinRoot.isAdjoinRoot f = { map := AdjoinRoot.mkₐ f, map_surjective := ⋯, ker_map := ⋯ }
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instZero : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → [Zero β] → Zero (α →ₘ[μ] β)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_Ψ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ),
  (W.map f).Ψ n = Polynomial.map (Polynomial.mapRingHom f) (W.Ψ n)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.prevn.eq_def : ∀ (x : String.Legacy.Iterator) (x_1 : ℕ),
  x.prevn x_1 =
    match x, x_1 with
    | it, 0 => it
    | it, i.succ => it.prev.prevn i
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidOpenTextDocumentParams : Type
-- Mathlib.Data.Set.Countable
Set.countable_univ_iff : ∀ {α : Type u}, Set.univ.Countable ↔ Countable α
-- Mathlib.Algebra.Opposites
AddOpposite.op_eq_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : α), AddOpposite.op a = 0 ↔ a = 0
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_ne_one : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial R]
  (x : M), (ExteriorAlgebra.ι R) x ≠ 1
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_comp_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.fst.comp AddMonoid.Coprod.inl = AddMonoidHom.id M
-- Init.Data.Function
Function.Injective.exists_leftInverse : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ [hα : Nonempty α], ∃ g, Function.LeftInverse g f
-- Mathlib.RingTheory.LocalRing.ResidueField.Instances
instIsAlgebraicQuotientIdealResidueField : ∀ {A : Type u_2} [inst : CommRing A] (p : Ideal A) [inst_1 : p.IsPrime], Algebra.IsAlgebraic (A ⧸ p) p.ResidueField
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.coe_id : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : MulZeroOneClass α], ⇑(OrderMonoidWithZeroHom.id α) = id
-- Std.Net.Addr
Std.Net.MACAddr.mk.sizeOf_spec : ∀ (octets : Vector UInt8 6), sizeOf { octets := octets } = 1 + sizeOf octets
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} (f g : X ⟶ Y), f.f = g.f → f = g
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.isIso_of_isIsos : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (f : A ⟶ B),
  CategoryTheory.IsIso f.hom₁ → CategoryTheory.IsIso f.hom₂ → CategoryTheory.IsIso f.hom₃ → CategoryTheory.IsIso f
-- Mathlib.LinearAlgebra.Dimension.RankNullity
exists_linearIndepOn_of_lt_rank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] {s : Set M},
  LinearIndepOn R id s → ∃ t, s ⊆ t ∧ Cardinal.mk ↑t = Module.rank R M ∧ LinearIndepOn R id t
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.toLower_inj : ∀ {α : Type u_1} {a b : α}, Topology.WithLower.toLower a = Topology.WithLower.toLower b ↔ a = b
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
/-- `agmSequences x y` is the sequence of (geometric, arithmetic) means
converging to the arithmetic-geometric mean starting from `x` and `y`.  -/
NNReal.agmSequences : NNReal → NNReal → ℕ → NNReal × NNReal
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
/-- An order-preserving isomorphism between the `ValueGroup₀` of a discrete valuation and `ℤᵐ⁰`.
TODO: rename this into lowerCamelCase.  -/
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {R : Type u_2} →
      [inst_1 : Ring R] →
        (v : Valuation R Γ) →
          [hv : v.IsRankOneDiscrete] → (MonoidWithZeroHom.ofClass v).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ)
-- Init.Data.List.ToArray
/-- Variant of `forM_toArray` with a side condition for the `stop` argument.  -/
List.forM_toArray' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {stop : ℕ} [inst : Monad m] (l : List α) (f : α → m PUnit.{u_1 + 1}),
  stop = l.toArray.size → Array.forM f l.toArray 0 stop = l.forM f
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_add_right : ∀ {α : Type u_1} {s t u : Multiset α}, Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u
-- Batteries.Data.String.Lemmas
String.utf8Len_le_of_sublist : ∀ {cs₁ cs₂ : List Char}, cs₁.Sublist cs₂ → String.utf8Len cs₁ ≤ String.utf8Len cs₂
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instFaithfulSMulSubtypeMem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_1}
  [inst_3 : SMul A α] [FaithfulSMul A α] (S : Subalgebra R A), FaithfulSMul (↥S) α
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.reindex_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C}
  (E : J.ZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀), (E.reindex e).toPreZeroHypercover = E.reindex e
-- Mathlib.RingTheory.AdicCompletion.Basic
IsPrecomplete.top : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M], IsPrecomplete ⊤ M
-- Mathlib.Order.Cover
Prod.mk_covBy_mk_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {a₁ a₂ : α} {b₁ b₂ : β},
  (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ioc : ∀ {α : Type u_1} {ι : Sort u_3} {ι' : Sort u_4} [inst : LinearOrder α] (f : ι → α) (g : ι' → α),
  IsPiSystem {S | ∃ i j, f i < g j ∧ Set.Ioc (f i) (g j) = S}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mk.inj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} A}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {inst_2 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} A'} {inst_4 : CategoryTheory.Category.{v₅, u₅} B'}
  {inst_5 : CategoryTheory.Category.{v₆, u₆} C'} {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {left : CategoryTheory.Functor A A'} {base : CategoryTheory.Functor B B'} {right : CategoryTheory.Functor C C'}
  {squareLeft :
    autoParam (CategoryTheory.CatCommSq F left base F') CategoryTheory.Limits.CatCospanTransform.squareLeft._autoParam}
  {squareRight :
    autoParam (CategoryTheory.CatCommSq G right base G')
      CategoryTheory.Limits.CatCospanTransform.squareRight._autoParam}
  {left_1 : CategoryTheory.Functor A A'} {base_1 : CategoryTheory.Functor B B'} {right_1 : CategoryTheory.Functor C C'}
  {squareLeft_1 :
    autoParam (CategoryTheory.CatCommSq F left_1 base_1 F')
      CategoryTheory.Limits.CatCospanTransform.squareLeft._autoParam}
  {squareRight_1 :
    autoParam (CategoryTheory.CatCommSq G right_1 base_1 G')
      CategoryTheory.Limits.CatCospanTransform.squareRight._autoParam},
  { left := left, base := base, right := right, squareLeft := squareLeft, squareRight := squareRight } =
      { left := left_1, base := base_1, right := right_1, squareLeft := squareLeft_1, squareRight := squareRight_1 } →
    left = left_1 ∧ base = base_1 ∧ right = right_1 ∧ squareLeft ≍ squareLeft_1 ∧ squareRight ≍ squareRight_1
-- Init.Control.Do
/-- A wrapper around `OptionT` signifying `continue` in a loop.  -/
ContinueT : (Type u_1 → Type u_2) → Type u_1 → Type u_2
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Functor composition on polynomial functors  -/
MvPFunctor.comp : {n m : ℕ} → MvPFunctor.{u} n → (Fin2 n → MvPFunctor.{u} m) → MvPFunctor.{u} m
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.pow_right_strictAnti : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (I : Ideal A), I ≠ ⊥ → I ≠ ⊤ → StrictAnti fun x => I ^ x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofZeros_left : ∀ {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),
  (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).left =
    CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves finite colimits, then `F.rightOp : C ⥤ Dᵒᵖ` preserves finite
limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.Limits.PreservesFiniteLimits F.rightOp
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- `lpTrimToLpMeasSubgroup` is a right inverse of `lpMeasSubgroupToLpTrim`.  -/
MeasureTheory.lpMeasSubgroupToLpTrim_right_inv : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0),
  Function.RightInverse (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm) (MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {k : α}, List.find? (fun x => x.1 == k) (Std.DHashMap.Raw.Const.toList ↑m) = none ↔ m.contains k = false
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Functor.PreservesPairwisePullbacks.mk : ∀ {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 : C}
  {R : CategoryTheory.Presieve X},
  autoParam
      (∀ ⦃Y Z : C⦄ ⦃f : Y ⟶ X⦄ ⦃g : Z ⟶ X⦄,
        R f → R g → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F)
      CategoryTheory.Functor.PreservesPairwisePullbacks.preservesLimit._autoParam →
    F.PreservesPairwisePullbacks R
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.levelNames : Lean.Elab.Term.SavedContext → List Lean.Name
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_eq_strictMap : ∀ {V : SSet.Truncated 2},
  SSet.Truncated.HomotopyCategory.morphismPropertyHomMk V =
    (CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk (SSet.OneTruncation₂ V)).strictMap
      (SSet.Truncated.HomotopyCategory.quotientFunctor V)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.flip_add : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f g : E →SL[σ₁₃] F →SL[σ₂₃] G),
  (f + g).flip = f.flip + g.flip
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_sub : ∀ {R : Type u_1} [inst : Ring R] {a b : R} [MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.C (a - b) = SkewPolynomial.C a - SkewPolynomial.C b
-- Mathlib.Data.Matrix.Block
Matrix.toBlocks_fromBlocks₁₁ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α), (Matrix.fromBlocks A B C D).toBlocks₁₁ = A
-- Mathlib.ModelTheory.Semantics
/-- A formula can be evaluated as true or false by giving values to each free variable.  -/
FirstOrder.Language.Formula.Realize : {L : FirstOrder.Language} → {M : Type w} → [L.Structure M] → {α : Type u'} → L.Formula α → (α → M) → Prop
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.orthogonal_top_eq_ker : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsRefl → B.orthogonal ⊤ = LinearMap.ker B
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.isPrivate : Lean.Elab.Visibility → Bool
-- Mathlib.Data.Real.Basic
Real.ofCauchy_intCast : ∀ (z : ℤ), { cauchy := ↑z } = ↑z
-- Mathlib.MeasureTheory.Measure.AEMeasurable
MeasurableEmbedding.aemeasurable_comp_iff : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : α → β} {g : β → γ},
  MeasurableEmbedding g → ∀ {μ : MeasureTheory.Measure α}, AEMeasurable (g ∘ f) μ ↔ AEMeasurable f μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst.eq_1 : ∀ (p : Lean.Grind.CommRing.Poly) (k : ℤ), p.addConst k = bif k == 0 then p else Lean.Grind.CommRing.Poly.addConst.go k p
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.truncLE'.truncLE'_hasHomology : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i : ι), (K.truncLE' e).HasHomology i
-- Mathlib.Order.Atoms
IsAtom.lt_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a x : α}, IsAtom a → (x < a ↔ x = ⊥)
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.coe_tsum_of_nonneg : ∀ {α : Type u_2} {L : SummationFilter α} {f : α → ℝ} (hf₁ : ∀ (n : α), 0 ≤ f n),
  NNReal.mk (∑'[L] (n : α), f n) ⋯ = ∑'[L] (n : α), NNReal.mk (f n) ⋯
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_5 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] [inst_6 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_7 : K.WEqualsLocallyBijective AddCommGrpCat] [inst_8 : F.Final] {I : Type u} (i : I) {Z : SheafOfModules R}
  (h : SheafOfModules.free I ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((SheafOfModules.pullback φ).map (SheafOfModules.ιFree i))
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.pullbackObjFreeIso φ I).hom h) =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.pullbackObjUnitToUnit φ)
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) h)
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
/-- `K.restrictionToTruncGE' e` is a quasi-isomorphism in degrees that are not at the boundary.  -/
HomologicalComplex.truncGE'.quasiIsoAt_restrictionToTruncGE' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (j : ι),
  ¬e.BoundaryGE j →
    ∀ [inst_4 : (K.restriction e).HasHomology j] [inst_5 : (K.truncGE' e).HasHomology j],
      QuasiIsoAt (K.restrictionToTruncGE' e) j
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : Inhabited α] [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k).get! a = if (k == a) = true then default else m.get! a
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.δToCycles_πE_assoc : ∀ {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_πE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.δToCycles_πE._auto_3) {Z : C}
  (h : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁)
      (CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  LinearIndependent S fun i j => (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map j)) (P.relation i))
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_toMatrix' : ∀ {A : Type u_5} [inst : CommRing A] {ι : Type u_7} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  (f : (ι → A) →ₗ[A] ι → A), (LinearMap.toMatrix' f).det = LinearMap.det f
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instIsLeftCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsLeftCancelMul α], IsLeftCancelMul αᵒᵈ
-- Mathlib.Analysis.Calculus.DSlope
continuousAt_dslope_same : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜}, ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.normProcs : Lean.Meta.Grind.Params → Array Lean.Meta.Simprocs
-- Mathlib.Order.BoundedOrder.Basic
ULift.instBot.eq_1 : ∀ {α : Type u} [inst : Bot α], ULift.instBot = { bot := { down := ⊥ } }
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.atomic_partSize : ∀ (n : ℕ), (OrderedFinpartition.atomic n).partSize = fun x => 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_iff_isSome_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∈ m ↔ (Std.DHashMap.Raw.Const.get? m a).isSome = true
-- Mathlib.Order.Filter.Prod
Filter.coprod.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β),
  f.coprod g = Filter.comap Prod.fst f ⊔ Filter.comap Prod.snd g
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- A continuous linear operator is self-adjoint iff it is equal to its adjoint.  -/
LinearMap.isSelfAdjoint_iff' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E}, IsSelfAdjoint A ↔ LinearMap.adjoint A = A
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addU.eq_1 : ∀ {F : Type u} [inst : Field F] (P Q : Fin 3 → F),
  WeierstrassCurve.Projective.addU P Q = -(P 1 * Q 2 - Q 1 * P 2) ^ 3 / (P 2 * Q 2)
-- Lean.Declaration
Lean.ConstantInfo.thmInfo.inj : ∀ {val val_1 : Lean.TheoremVal}, Lean.ConstantInfo.thmInfo val = Lean.ConstantInfo.thmInfo val_1 → val = val_1
-- Mathlib.Algebra.Free
FreeMagma.instTraversable : Traversable FreeMagma
-- Mathlib.Order.Category.OmegaCompletePartialOrder
/-- The equalizer inclusion function as a `ContinuousHom`.  -/
ωCPO.HasEqualizers.equalizerι : {α : Type u_1} →
  {β : Type u_2} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : OmegaCompletePartialOrder β] → (f g : α →𝒄 β) → { a // f a = g a } →𝒄 α
-- Mathlib.GroupTheory.Focal
/-- The power map `y ↦ y^n` is surjective on `P/P*` because `gcd(n, p) = 1`.  -/
Subgroup.focalSubgroupOf.pow_index_surjective : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [(↑P).FiniteIndex],
  Function.Surjective fun y => y ^ (↑P).index
-- Std.Sat.AIG.Basic
/-- Given a `cache`, valid with respect to some `decls`, we can extend the `decls`
and the `cache` at the same time with the same values and remain valid.
 -/
Std.Sat.AIG.Cache.insert : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (decls : Array (Std.Sat.AIG.Decl α)) →
        Std.Sat.AIG.Cache α decls → (decl : Std.Sat.AIG.Decl α) → Std.Sat.AIG.Cache α (decls.push decl)