mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.rangeS_eq_top : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S},
  f.rangeS = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.smul.congr_simp : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  [inst_5 : VAdd Γ Γ'] [inst_6 : IsOrderedCancelVAdd Γ Γ'] (s s_1 : HahnSeries.SummableFamily Γ R α),
  s = s_1 → ∀ (t t_1 : HahnSeries.SummableFamily Γ' V β), t = t_1 → s.smul t = s_1.smul t_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k} [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (Std.DHashMap.ofList l).get! k' = cast ⋯ v
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.flipHom_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P}
  (f : M →* N →* P), MonoidHom.flipHom f = f.flip
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map₂_coe_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β), WithZero.map₂ f ↑a ↑b = ↑(f a b)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.instInhabitedOrdSet.default : {α : Type} → {inst : Hashable α} → {inst_1 : BEq α} → Lean.Meta.Try.Collector.OrdSet α
-- Mathlib.Topology.Connected.LocallyPathConnected
LocallyPathConnectedSpace.of_bases : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {p : X → ι → Prop} {s : X → ι → Set X},
  (∀ (x : X), (nhds x).HasBasis (p x) (s x)) →
    (∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)) → LocallyPathConnectedSpace X
-- Mathlib.Computability.Primrec.List
Primrec.list_foldr : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → List β} {g : α → σ} {h : α → β × σ → σ},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.foldr (fun b s => h a (b, s)) (g a) (f a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negDblY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) (u : R),
  W'.negDblY (u • P) = u ^ 4 * W'.negDblY P
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map_bot : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), ⊥.map f = AlgebraicGeometry.Scheme.Hom.ker f
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- The Cartesian product of two nonarchimedean groups is nonarchimedean.  -/
NonarchimedeanAddGroup.Prod.instNonarchimedeanAddGroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [NonarchimedeanAddGroup G] {K : Type u_3}
  [inst_3 : AddGroup K] [inst_4 : TopologicalSpace K] [NonarchimedeanAddGroup K], NonarchimedeanAddGroup (G × K)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (s : Set Ω) (i : ι),
  MeasurableSet (s ∩ {ω | τ ω ≤ ↑i}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.union_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s₁ s₂ : Set α} {t : Set β}, (s₁ ∪ s₂) +ᵥ t = (s₁ +ᵥ t) ∪ (s₂ +ᵥ t)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddGroup.addRightReflectLE_of_addRightMono : ∀ {N : Type u_2} [inst : AddGroup N] [inst_1 : LE N] [AddRightMono N], AddRightReflectLE N
-- Mathlib.FieldTheory.Relrank
IntermediateField.lift_relrank_comap : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) (B : IntermediateField F L),
  Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank B) =
    Cardinal.lift.{w, v} (A.relrank (IntermediateField.map f B))
-- Mathlib.Analysis.Normed.Group.Hom
/-- Opposite of a normed group hom.  -/
NormedAddGroupHom.neg : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → Neg (NormedAddGroupHom V₁ V₂)
-- Mathlib.Data.List.Lattice
List.bagInter_nil : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.bagInter [] = []
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.linsts : ProofWidgets.ExprWithCtx → Lean.LocalInstances
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.enumMember : Lean.Lsp.SemanticTokenType
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.continuousAdd : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [ContinuousAdd M] (S : AddSubmonoid M),
  ContinuousAdd ↥S
-- Mathlib.Topology.Bornology.Hom
/-- `LocallyBoundedMapClass F α β` states that `F` is a type of bounded maps.

You should extend this class when you extend `LocallyBoundedMap`.  -/
LocallyBoundedMapClass : (F : Type u_6) →
  (α : outParam (Type u_7)) → (β : outParam (Type u_8)) → [Bornology α] → [Bornology β] → [FunLike F α β] → Prop
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type E₇.

The corresponding Coxeter-Dynkin diagram is:
```
                o
                |
    o --- o --- o --- o --- o --- o
```
 -/
CoxeterMatrix.E₇ : CoxeterMatrix (Fin 7)
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DTreeMap.Raw.getKey! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap.Raw α β cmp → α → α
-- Mathlib.RingTheory.Coalgebra.TensorProduct
_private.Mathlib.RingTheory.Coalgebra.TensorProduct.0.Coalgebra.«term_▷_» : Lean.TrailingParserDescr
-- Mathlib.Geometry.Manifold.Bordism
/-- A **singular manifold** on a topological space `X` is a pair `(M, f)` of a closed
`C^k`-manifold `M` modelled on `I` together with a continuous map `M → X`.
If we wish to emphasize the model, we will speak of a singular `I`-manifold.

In practice, one commonly wants to take `k=∞` (as then e.g. the intersection form is a powerful tool
to compute bordism groups; for the definition, this makes no difference.)

This is parametrised on the universe `M` lives in; ensure `u` is the first universe argument.  -/
SingularManifold : (X : Type u_1) →
  [TopologicalSpace X] →
    WithTop ℕ∞ →
      {E : Type u_2} →
        {H : Type u_3} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [FiniteDimensional ℝ E] →
                [inst_3 : TopologicalSpace H] → ModelWithCorners ℝ E H → Type (max (max (u + 1) u_1) u_3)
-- Init.Data.Int.Lemmas
Int.ofNat_eq_zero : ∀ {n : ℕ}, ↑n = 0 ↔ n = 0
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.mk.injEq : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} (index : ιₚ)
  (groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries) (index_1 : ιₚ)
  (groupElts_1 : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index_1)).subtype (↑ps index_1).symmetries),
  ({ index := index, groupElts := groupElts } = { index := index_1, groupElts := groupElts_1 }) =
    (index = index_1 ∧ groupElts ≍ groupElts_1)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rcc : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toList[i]! = if i < (n + 1 - m).toNat then m + ↑i else 0
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.opENorm_comp_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : NontriviallyNormedField 𝕜₃]
  [inst_3 : SeminormedAddCommGroup E] [inst_4 : SeminormedAddCommGroup F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomIsometric σ₁₂]
  [inst_11 : RingHomIsometric σ₂₃] [inst_12 : RingHomIsometric σ₁₃] (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F),
  ‖h ∘SL f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.unionFuel.match_1.eq_1 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x₁ x₂ : Lean.Grind.AC.Var)
  (h_1 : (x₁ x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂))
  (h_2 :
    (x₁ x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂))
  (h_4 :
    (x₁ : Lean.Grind.AC.Var) →
      (s₁ : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) →
          (s₂ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂)),
  (match Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ with
    | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ => h_1 x₁ x₂
    | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s => h_2 x₁ x s
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ => h_3 x s x₂
    | Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ => h_4 x₁ s₁ x₂ s₂) =
    h_1 x₁ x₂
-- Mathlib.Tactic.Translate.Core
/-- Warn the user when the declaration has an attribute.  -/
Mathlib.Tactic.Translate.warnAttrCore : Lean.Syntax → (Lean.Environment → Lean.Name → Bool) → Lean.Name → Lean.Name → Lean.Name → Lean.Name → Lean.CoreM Unit
-- Mathlib.Analysis.Normed.Group.NullSubmodule
nullAddSubgroup.eq_1 : ∀ (M : Type u_1) [inst : SeminormedAddCommGroup M],
  nullAddSubgroup M = { carrier := {x | ‖x‖ = 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Analysis.Normed.Group.Uniform
nndist_add_add_le : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E),
  nndist (a₁ + a₂) (b₁ + b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_refl : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P],
  ⇑(AffineIsometryEquiv.refl 𝕜 P) = id
-- Init.Prelude
/-- Exception monads provide the ability to throw errors and handle errors.

In this class, `ε` is an `outParam`, which means that it is inferred from `m`. `MonadExceptOf ε`
provides the same operations, but allows `ε` to influence instance synthesis.

`MonadExcept.tryCatch` is used to desugar `try ... catch ...` steps inside `do`-blocks when the
handlers do not have exception type annotations.
 -/
MonadExcept : outParam (Type u) → (Type v → Type w) → Type (max (max u (v + 1)) w)
-- Mathlib.Topology.MetricSpace.Defs
dist_ofMul : ∀ {X : Type u_1} [inst : Dist X] (a b : X), dist (Additive.ofMul a) (Additive.ofMul b) = dist a b
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- **Alias** of `Valuation.Integers.maximalIdeal_pow_eq_setOfPred_le_v_algebraMap_pow`. -/
Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow : ∀ {K : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O K] {v : Valuation K Γ₀} (hv : v.Integers O)
  [inst_4 : IsDiscreteValuationRing O] {ϖ : O},
  Irreducible ϖ →
    ∀ (n : ℕ), ↑(IsLocalRing.maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}
-- Mathlib.Order.Closure
/-- Conjugating `ClosureOperators` on `α` and on `β` by a fixed isomorphism
`e : α ≃o β` gives an equivalence `ClosureOperator α ≃ ClosureOperator β`.  -/
OrderIso.equivClosureOperator : {α : Type u_4} →
  {β : Type u_5} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → ClosureOperator α ≃ ClosureOperator β
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.finsetProd_singleton : ∀ {M : Type u_5} {ι : Type u_6} [inst : CommMonoid M] (s : Finset ι) (I : ι → M), ∏ i ∈ s, {I i} = {∏ i ∈ s, I i}
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, `A'` and `B'` are contained in `A` and `B`,
respectively, then `A'` and `B'` are also linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  {A B A' B' : IntermediateField F E}, A.LinearDisjoint ↥B → A' ≤ A → B' ≤ B → A'.LinearDisjoint ↥B'
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `M` is finite free over a PID `R`, then for any submodule `N` of the same rank,
we can find basis for `M` and `N` with the same indexing such that the inclusion map
is a square diagonal matrix.

See also `Submodule.smithNormalFormOfRankEq` for a version of this theorem that returns
a `Basis.SmithNormalForm`.
 -/
Submodule.exists_smith_normal_form_of_rank_eq : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsDomain R] [IsPrincipalIdealRing R] {N : Submodule R M} [Finite ι] (b : Module.Basis ι R M),
  Module.finrank R ↥N = Module.finrank R M → ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
-- Mathlib.Topology.GDelta.Basic
/-- A set `s` is called *residual* if it includes a countable intersection of dense open sets.  -/
residual : (X : Type u_5) → [TopologicalSpace X] → Filter X
-- Mathlib.Order.BooleanAlgebra.Basic
BooleanAlgebra.toComplementedLattice : ∀ {α : Type u} [inst : BooleanAlgebra α], ComplementedLattice α
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `upperSemicontinuousWithinAt_iff_limsup_le`. -/
UpperSemicontinuousWithinAt.limsup_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ]
  {f : α → γ}, UpperSemicontinuousWithinAt f s x → Filter.limsup f (nhdsWithin x s) ≤ f x
-- Mathlib.Algebra.Category.ModuleCat.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} [inst_1 : SizeOf R] (hom' : ↑M →ₗ[R] ↑N),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insert_ne_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.insert k v ≠ ∅
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectL_prodMkRight : ∀ {α : Type u_1} {mα : MeasurableSpace α} {γ : Type u_4} {mγ : MeasurableSpace γ} (β : Type u_6)
  [inst : MeasurableSpace β] (κ : ProbabilityTheory.Kernel α γ) (b : β),
  (ProbabilityTheory.Kernel.prodMkRight β κ).sectL b = κ
-- Mathlib.Data.EReal.Basic
instDenselyOrderedEReal : DenselyOrdered EReal
-- Mathlib.Topology.UniformSpace.Equiv
/-- If two sets are equal, then they are uniformly equivalent.  -/
UniformEquiv.setCongr : {α : Type u} → [inst : UniformSpace α] → {s t : Set α} → s = t → ↑s ≃ᵤ ↑t
-- Std.Data.HashMap.Lemmas
Std.HashMap.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  Std.HashMap.forIn f init m = forIn m.toArray init fun a b => f a.1 a.2 b
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_erase_eq_of_not_compare_eq_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, ¬cmp k (t.min ⋯) = Ordering.eq → (t.erase k).min he = t.min ⋯
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex₂.homMk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (f f_1 : K.toGradedObject ⟶ L.toGradedObject) (e_f : f = f_1)
  (comm₁ :
    ∀ (i₁ i₁' : I₁) (i₂ : I₂),
      c₁.Rel i₁ i₁' →
        CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.d i₁ i₁').f i₂) =
          CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (f (i₁', i₂)))
  (comm₂ :
    ∀ (i₁ : I₁) (i₂ i₂' : I₂),
      c₂.Rel i₂ i₂' →
        CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.X i₁).d i₂ i₂') =
          CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (f (i₁, i₂'))),
  HomologicalComplex₂.homMk f comm₁ comm₂ = HomologicalComplex₂.homMk f_1 ⋯ ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.filter! f t) k =
    (Std.DTreeMap.Internal.Impl.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_consₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ (a : α) (b : β a),
      (Std.DHashMap.Internal.toListModel (↑(m.consₘ a b)).buckets).Perm
        (⟨a, b⟩ :: Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_int64ToInt : ∀ (x : Int64) {h₁ : ISize.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ ISize.maxValue.toInt},
  ISize.ofIntLE x.toInt h₁ h₂ = x.toISize
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.ofPiFork_π_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left}
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.R),
  (CategoryTheory.Limits.Multifork.ofPiFork a).π.app (CategoryTheory.Limits.WalkingMulticospan.right i) =
    CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i))
-- Mathlib.Algebra.Module.Presentation.Cokernel
/-- Given a linear map `f : M₁ →ₗ[A] M₂`, a presentation of `M₂` and a choice
of generators of `M₁`, this structure specifies a lifting of the image by `f`
of each generator of `M₁` as a linear combination of the generators of `M₂`.  -/
Module.Presentation.CokernelData : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                Module.Presentation A M₂ → (M₁ →ₗ[A] M₂) → {ι : Type w₁} → (ι → M₁) → Type (max (max u w₁) w₂₀)
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.vaddAntidiagonal_mono_left : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s u : Set G} {t : Set P} (a : P),
  u ⊆ s →
    ∀ (hst : (s.vaddAntidiagonal t a).Finite) (hut : (u.vaddAntidiagonal t a).Finite),
      Finset.VAddAntidiagonal a hut ⊆ Finset.VAddAntidiagonal a hst
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.lift_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : Type u₁} [inst_1 : CategoryTheory.Groupoid G]
  (φ : CategoryTheory.Functor C G), (CategoryTheory.FreeGroupoid.of C).comp (CategoryTheory.FreeGroupoid.lift φ) = φ
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.find? : Lean.AsyncConsts✝ → Lean.Name → Option Lean.AsyncConst✝
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k a : α} {v : β},
  Std.DTreeMap.Const.get! (t.insert k v) a = if cmp k a = Ordering.eq then v else Std.DTreeMap.Const.get! t a
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.continuous_toFun : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] (self : α →Co β), Continuous self.toFun
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.MeasurePreserving (⇑(NumberField.mixedEmbedding.euclidean.toMixed K).symm) MeasureTheory.volume
    MeasureTheory.volume
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.instIsStableUnderShiftIntPlus : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (CochainComplex.plus C).IsStableUnderShift ℤ
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.principal_F : ∀ {α : Type u_1} (s : Set α) (u : Unit), (Filter.Realizer.principal s).F.f u = s
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- An auxiliary lemma for `linearIndependent_le_basis`:
we handle the case where the basis `b` is infinite.
 -/
linearIndependent_le_infinite_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type w} (b : Module.Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M),
  LinearIndependent R v → Cardinal.mk κ ≤ Cardinal.mk ι
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.NamedLinter.mk.inj : ∀ {toLinter : Batteries.Tactic.Lint.Linter} {name declName : Lean.Name} {toLinter_1 : Batteries.Tactic.Lint.Linter}
  {name_1 declName_1 : Lean.Name},
  { toLinter := toLinter, name := name, declName := declName } =
      { toLinter := toLinter_1, name := name_1, declName := declName_1 } →
    toLinter = toLinter_1 ∧ name = name_1 ∧ declName = declName_1
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.norm_compSL_le : ∀ {𝕜 : 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 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomIsometric σ₂₃]
  [inst_11 : RingHomIsometric σ₁₃] [inst_12 : RingHomIsometric σ₁₂], ‖ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃‖ ≤ 1
-- Mathlib.Data.Finset.Union
Finset.disjoint_biUnion_left : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (f : α → Finset β) (t : Finset β),
  Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
-- Lean.Compiler.IR.Format
_private.Lean.Compiler.IR.Format.0.Lean.IR.formatLitVal : Lean.IR.LitVal → Std.Format
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.eval_one : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁), F.eval 1 = p₁
-- Mathlib.Topology.Clopen
/-- **Alias** of the forward direction of `isClopen_iff_frontier_eq_empty`. -/
IsClopen.frontier_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s → frontier s = ∅
-- Mathlib.Order.CompleteLattice.Lemmas
biInf_sup_le_biInf_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (s : Set β) (a : α),
  (⨅ i ∈ s, f i) ⊔ a ≤ ⨅ i ∈ s, f i ⊔ a
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasStrictDerivAt.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {f : 𝕜 → ℂ} {f' : ℂ} {x : 𝕜},
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) * f') x
-- Aesop.Search.Expansion.Norm
Aesop.applyDiffToForwardState : Aesop.GoalDiff → Aesop.NormM Unit