mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp_assoc : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp._auto_3) {Z : C}
  (h :
    X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₄ i₅ hi₀₁ hi₁₂ ⋯ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂) h
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.isCompl_comap_subtype_of_isCompl_of_le : ∀ {R : Type u_10} {M : Type u_11} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p q r : Submodule R M}, IsCompl q r → q ≤ p → IsCompl (Submodule.comap p.subtype q) (Submodule.comap p.subtype r)
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.instBEqSplitStatus.beq : Lean.Meta.Grind.SplitStatus → Lean.Meta.Grind.SplitStatus → Bool
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- If `χ` is a multiplicative character with `χ^n = 1` and `μ` is a primitive `n`th root
of unity, then, for `a ≠ 0`, there is some `k` such that `χ a = μ^k`.  -/
MulChar.exists_apply_eq_pow : ∀ {F : Type u_1} [inst : Field F] [Finite F] {R : Type u_2} [inst_2 : CommRing R] [IsDomain R] {χ : MulChar F R} {n : ℕ}
  [NeZero n], χ ^ n = 1 → ∀ {μ : R}, IsPrimitiveRoot μ n → ∀ {a : F}, a ≠ 0 → ∃ k < n, χ a = μ ^ k
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β},
  (m.modify k f)[k']? = if (k == k') = true then Option.map f m[k]? else m[k']?
-- Lean.Meta.Sorry
Lean.Meta.SorryLabelView.encode : Lean.Meta.SorryLabelView → Lean.CoreM Lean.Name
-- Std.Internal.Parsec.String
/-- Skips the given char.
 -/
Std.Internal.Parsec.String.skipChar : Char → Std.Internal.Parsec.String.Parser Unit
-- Mathlib.Order.ModularLattice
IsLowerModularLattice.to_isWeakLowerModularLattice : ∀ {α : Type u_1} [inst : Lattice α] [IsLowerModularLattice α], IsWeakLowerModularLattice α
-- Std.Data.HashMap.Lemmas
Std.HashMap.all_eq_false_iff_exists_mem_getKey_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {p : α → β → Bool}, m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p (m.getKey a h) m[a] = false
-- Lean.Elab.DocString
/-- The local context.

The `MonadLift TermElabM DocM` instance runs the lifted action in this context, so elaboration
commands that mutate this state cause it to take effect in subsequent commands.
 -/
Lean.Doc.State.lctx : Lean.Doc.State → Lean.LocalContext
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J RingCat} →
      {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop} →
        {a a_1 : RingCat.Colimits.Prequotient F} → RingCat.Colimits.Relation F a a_1 → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
max_mul_mul_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulRightMono α] (a b c : α), max (a * c) (b * c) = max a b * c
-- Mathlib.Algebra.Star.Basic
/-- Given a type endowed with `star`, that `star` is involutive if it admits an injective map that
preserves `star` to a type with whose `star` is involutive. See note [reducible non-instances].  -/
Function.Injective.involutiveStar : {R : Type u} →
  {S : Type v} →
    (f : R → S) →
      [inst : Star R] →
        [inst_1 : InvolutiveStar S] → Function.Injective f → (∀ (x : R), f (star x) = star (f x)) → InvolutiveStar R
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.embed.eq_1 : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible],
  ValuativeRel.ValueGroupWithZero.embed v =
    {
      toFun :=
        ValuativeRel.ValueGroupWithZero.lift
          (fun r s =>
            (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) r /
              (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) ↑s)
          ⋯,
      map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Projective
/-- The categorical notion of projective object agrees with the explicit module-theoretic notion.  -/
IsProjective.iff_projective : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] (P : Type v) [inst_2 : AddCommGroup P] [inst_3 : Module R P],
  Module.Projective R P ↔ CategoryTheory.Projective (ModuleCat.of R P)
-- Init.Data.Int.Lemmas
Int.neg_mul_comm : ∀ (a b : ℤ), -a * b = a * -b
-- Mathlib.Topology.Order
TopologicalSpace.eq_top_iff_forall_inseparable : ∀ {α : Type u} {t : TopologicalSpace α}, t = ⊤ ↔ ∀ (x y : α), Inseparable x y
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_antisymm : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
  m.sPolynomial f g = -m.sPolynomial g f
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.inner_map_map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H)
  (x y : TensorProduct 𝕜 E F),
  inner 𝕜 ((TensorProduct.map f.toLinearMap g.toLinearMap) x) ((TensorProduct.map f.toLinearMap g.toLinearMap) y) =
    inner 𝕜 x y
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₄Unchecked : UInt8 → UInt8 → UInt8 → UInt8 → UInt32
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.of_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsClosedEmbedding g → (Topology.IsClosedEmbedding (g ∘ f) ↔ Topology.IsClosedEmbedding f)
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_le_op_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S₁ S₂ : Subalgebra R A}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
_private.Mathlib.CategoryTheory.Triangulated.SpectralObject.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_3 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt : 0 < n + 1 + 1) (j : ℕ)
  (hj : j + 2 < n + 1 + 1) (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩)
  (h_1 : (isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_1⟩, x => h_1 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨1, isLt_1⟩, x => h_2 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_3 isLt j hj x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.nodup_toList : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {a : α}, a<...*.toList.Nodup
-- Mathlib.Analysis.Complex.Exponential
Complex.norm_exp_ofReal : ∀ (x : ℝ), ‖Complex.exp ↑x‖ = Real.exp x
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instSub : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N' : Type u_6} → [inst_3 : AddCommGroup N'] → [inst_4 : Module R N'] → {ι : Type u_7} → Sub (M [⋀^ι]→ₗ[R] N')
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The algebra isomorphism between multivariable polynomials in `Option S₁` and
multivariable polynomials with coefficients in polynomials.
 -/
MvPolynomial.optionEquivRight : (R : Type u) → (S₁ : Type v) → [inst : CommSemiring R] → MvPolynomial (Option S₁) R ≃ₐ[R] MvPolynomial S₁ (Polynomial R)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddZeroClass : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddZeroClass M] → AddZeroClass (l.Germ M)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.inseparable_extension_coe : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f → ∀ (x : α), Inseparable (UniformSpace.Completion.extension f ↑x) (f x)
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.prodMap.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N'),
  f.prodMap g = (f.comp (AddMonoidHom.fst M N)).prod (g.comp (AddMonoidHom.snd M N))
-- Mathlib.Algebra.Homology.Embedding.Restriction
ComplexShape.Embedding.instAdditiveHomologicalComplexRestrictionFunctor : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : e.IsRelIff] [inst_2 : CategoryTheory.Preadditive C],
  (e.restrictionFunctor C).Additive
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.wf : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (a : 0 < m.buckets.size)
  (a_1 : ∀ [EquivBEq α] [LawfulHashable α], Std.DHashMap.Internal.Raw.WFImp m), Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_nat : ∀ (n : ℕ), Encodable.decode n = some n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ \ m₂},
  Std.DHashMap.Raw.Const.get (m₁.diff m₂) k h_mem = Std.DHashMap.Raw.Const.get m₁ k ⋯
-- Mathlib.Data.PFun
/-- Product of partial functions.  -/
PFun.prodLift : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α →. β) → (α →. γ) → α →. β × γ
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_succ_eq_succ_sum : ∀ (n : ℕ), Nat.fib (n + 1) = ∑ k ∈ Finset.range n, Nat.fib k + 1
-- Mathlib.Order.WithBotTop
WithBotTop.coe_ne_bot : ∀ {ι : Type u_1} (a : ι), WithBotTop.coe a ≠ ⊥
-- Init.Data.Array.Lemmas
Array.size_filter_le : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (Array.filter p xs).size ≤ xs.size
-- Init.Data.Int.Order
Int.add_lt_iff : ∀ {a b c : ℤ}, a + b < c ↔ a < -b + c
-- Mathlib.Algebra.Group.Action.Pretransitive
MulAction.instIsPretransitiveOfSubsingleton : ∀ {M : Type u_5} {α : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α] [Subsingleton α],
  MulAction.IsPretransitive M α
-- Mathlib.Topology.MetricSpace.Thickening
/-- The δ-thickening of the complement of the δ-thickening of a set is contained in the complement
of the set.  -/
Metric.thickening_compl_thickening_self_subset_compl : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α), Metric.thickening δ (Metric.thickening δ E)ᶜ ⊆ Eᶜ
-- Mathlib.Control.Fold
Traversable.foldl.eq_1 : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] (f : α → β → α) (x : α) (xs : t β),
  Traversable.foldl f x xs = (Traversable.foldMap (Monoid.Foldl.mk ∘ flip f) xs).get x
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_pure_interval : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑(NonemptyInterval.pure a) = Interval.pure a
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.coevaluation_evaluation_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.ExactPairing X Y] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (η_ X Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ X Y) Y) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv h)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.QuotientAction.mk : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : Monoid X] [inst_2 : MulAction X G] {H : Subgroup G},
  (∀ (b : X) {a a' : G}, a⁻¹ * a' ∈ H → (b • a)⁻¹ * b • a' ∈ H) → MulAction.QuotientAction X H
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.abel : Lean.ParserDescr
-- Mathlib.Order.Filter.Pointwise
Filter.pure_smul_pure : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {a : α} {b : β}, pure a • pure b = pure (a • b)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.rank.eq_1 : ∀ {α : Type u_1}, Batteries.BinomialHeap.Imp.HeapNode.nil.rank = 0
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- Every regular measure is induced by a positive linear functional on `C_c(X, ℝ)`.
That is, `RealRMK.rieszMeasure` is a surjective function onto regular measures.  -/
RealRMK.rieszMeasure_integralPositiveLinearMap : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  {μ : MeasureTheory.Measure X} [inst_4 : LocallyCompactSpace X] [inst_5 : μ.Regular],
  RealRMK.rieszMeasure (CompactlySupportedContinuousMap.integralPositiveLinearMap μ) = μ
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- The trace of a finite extension of integrally closed domains `B/A` is the restriction of
the trace on `Frac(B)/Frac(A)` onto `B/A`. See `Algebra.algebraMap_intTrace`.  -/
Algebra.intTrace : (A : Type u_1) →
  (B : Type u_6) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [IsDomain A] →
            [IsIntegrallyClosed A] →
              [IsDomain B] → [IsIntegrallyClosed B] → [Module.Finite A B] → [Module.IsTorsionFree A B] → B →ₗ[A] A
-- Mathlib.FieldTheory.Relrank
/-- **Alias** of the reverse direction of `IntermediateField.relfinrank_eq_one_iff`. -/
IntermediateField.relfinrank_eq_one_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  B ≤ A → A.relfinrank B = 1
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instSemilatticeInfFiniteIndexNormalAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → SemilatticeInf (FiniteIndexNormalAddSubgroup G)
-- Mathlib.Topology.LocallyFinite
LocallyFinite.closure_iUnion : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → closure (⋃ i, f i) = ⋃ i, closure (f i)
-- Mathlib.Data.Int.GCD
/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`.  -/
Int.gcdB : ℤ → ℤ → ℤ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Neg
Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (input : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg aig input =
    Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig input).aig
      { lhs := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig input).vec,
        rhs :=
          Std.Tactic.BVDecide.BVExpr.bitblast.blastConst (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig input).aig
            1#w }
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.delabJsxChildren : Lean.PrettyPrinter.Delaborator.DelabM (Array (Lean.TSyntax `proofWidgetsJsxChild))
-- Lean.Meta.Tactic.Grind.Types
/-- Current source of case-splits.  -/
Lean.Meta.Grind.Context.splitSource : Lean.Meta.Grind.Context → Lean.Meta.Grind.SplitSource
-- Std.Http.Protocol.H1.Parser
Std.Http.Protocol.H1.TakeResult.complete.inj : ∀ {data data_1 : ByteSlice},
  Std.Http.Protocol.H1.TakeResult.complete data = Std.Http.Protocol.H1.TakeResult.complete data_1 → data = data_1
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mker.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f f_1 : F), f = f_1 → MonoidHom.mker f = MonoidHom.mker f_1
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_obj_X₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₄ = f.right.right
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.nil`.  -/
Tree.nil : {α : Type u} → Tree α
-- Mathlib.Topology.UniformSpace.Closeds
UniformContinuous.nonemptyCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β}
  (hf : UniformContinuous f), UniformContinuous (TopologicalSpace.NonemptyCompacts.map f ⋯)
-- Mathlib.SetTheory.Lists
Lists.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (Lists α)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYoneda_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) {X Y : ℰ} (f : X ⟶ Y) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Presheaf.restrictedULiftYoneda A).map f).app X_1 =
    TypeCat.ofHom fun x => { down := CategoryTheory.CategoryStruct.comp x.down f }
-- Lean.Parser.Do
Lean.Parser.Term.doIdDecl : Lean.Parser.Parser
-- Mathlib.Algebra.Order.Archimedean.Class
_private.Mathlib.Algebra.Order.Archimedean.Class.0.FiniteArchimedeanClass.lift.match_1.splitter : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        (motive : FiniteArchimedeanClass M → Sort u_2) →
          (x : FiniteArchimedeanClass M) → ((A : ArchimedeanClass M) → (hA : A ≠ ⊤) → motive ⟨A, hA⟩) → motive x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → (m₁.diff m₂).getKey! k = default
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ιChainComplex_toNormalizedChainComplex_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) ((X.toNormalizedChainComplex R).f n) =
    X.ιNormalizedChainComplex x
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_of_differentiable_iteratedFDeriv : ∀ {𝕜 : 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 : ℕ∞}, (∀ (m : ℕ), ↑m ≤ n → Differentiable 𝕜 (iteratedFDeriv 𝕜 m f)) → ContDiff 𝕜 (↑n) f
-- Mathlib.Algebra.Tropical.Lattice
instSemilatticeInfTropical : {R : Type u_1} → [SemilatticeInf R] → SemilatticeInf (Tropical R)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackComp.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : P.IsStableUnderBaseChangeAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong g] [inst_4 : P.HasPullbacksAlong f] [inst_5 : P.HasPullbacksAlong g]
  [inst_6 : Q.RespectsIso] [inst_7 : Q.IsStableUnderBaseChange] (fg : X ⟶ Z)
  (hfg : fg = CategoryTheory.CategoryStruct.comp f g),
  CategoryTheory.MorphismProperty.Over.pullbackComp f g fg hfg =
    CategoryTheory.MorphismProperty.Over.pullbackComp f g fg hfg
-- Mathlib.Order.UpperLower.Closure
LowerSet.erase_idem : ∀ {α : Type u_1} [inst : Preorder α] (s : LowerSet α) (a : α), (s.erase a).erase a = s.erase a
-- Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceWWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X : C}
  (R : (HomotopicalAlgebra.CofibrantObject.localizerMorphism C).LeftResolution X),
  HomotopicalAlgebra.WeakEquivalence R.w
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.two_mul_arctan_inv_3_add_arctan_inv_7 : 2 * Real.arctan 3⁻¹ + Real.arctan 7⁻¹ = Real.pi / 4
-- Std.Http.Data.Status
/-- 508 Loop Detected
 -/
Std.Http.Status.loopDetected : Std.Http.Status
-- Mathlib.SetTheory.Cardinal.ENat
/-- Coercion `ℕ∞ → Cardinal`. It sends natural numbers to natural numbers and `⊤` to `ℵ₀`.

See also `Cardinal.ofENatHom` for a bundled homomorphism version.  -/
Cardinal.ofENat : ℕ∞ → Cardinal.{u_1}
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.extendCone_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {X Y : CategoryTheory.Limits.Cone (F.comp G)} (f : X ⟶ Y),
  (CategoryTheory.Functor.Initial.extendCone.map f).hom = f.hom
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.isZeroOrProbabilityMeasure_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.IsZeroOrProbabilityMeasure (μ.tilted f)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.nonMemberSubfamily_union : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 ℬ : Finset (Finset α)),
  Finset.nonMemberSubfamily a (𝒜 ∪ ℬ) = Finset.nonMemberSubfamily a 𝒜 ∪ Finset.nonMemberSubfamily a ℬ