mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanAlgebra.Defs
/-- An alternative constructor for Boolean algebras:
a distributive lattice that is complemented is a Boolean algebra.

This is not an instance, because it creates data using choice.
 -/
DistribLattice.booleanAlgebraOfComplemented : (α : Type u) → [inst : DistribLattice α] → [inst_1 : BoundedOrder α] → [ComplementedLattice α] → BooleanAlgebra α
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul.go.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  (match 0 with
    | 0 => h_1 ()
    | fuel.succ => h_2 fuel) =
    h_1 ()
-- Mathlib.Order.Disjoint
Codisjoint.left_le_of_le_inf_left : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderTop α] {a b c : α}, b ⊓ a ≤ c → Codisjoint b c → a ≤ c
-- Init.Data.BitVec.Lemmas
BitVec.toNat_neg_lt_of_msb : ∀ {w : ℕ} (x : BitVec w), x.msb = true → (-x).toNat ≤ 2 ^ (w - 1)
-- Mathlib.Data.Complex.Basic
/-- We use a nonstandard formula for the `ℕ` and `ℤ` actions to make sure there is no
diamond from the other actions they inherit through the `ℝ`-action on `ℂ` and action transitivity
defined in `Data.Complex.Module`.  -/
Complex.instNontrivial : Nontrivial ℂ
-- Mathlib.Analysis.Complex.Norm
Complex.equiv_limAux : ∀ (f : CauSeq ℂ fun x => ‖x‖), f ≈ CauSeq.const (fun x => ‖x‖) (Complex.limAux f)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.symm_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), α.symm.hom = α.inv
-- Mathlib.Data.PEquiv
PEquiv.mem_iff_mem : ∀ {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β}, a ∈ f.symm b ↔ b ∈ f a
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.GenPatternInfo.mk : Bool → ℕ → ℕ → Lean.Meta.Grind.GenPatternInfo
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The inclusion of the space `𝓓^{n}_{K}(E, F)` into the space `E →ᵇ F` of bounded continuous
functions as a continuous `𝕜`-linear map.  -/
ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    {n : ℕ∞} →
                      {K : TopologicalSpace.Compacts E} →
                        ContDiffMapSupportedIn E F n K →L[𝕜] BoundedContinuousFunction E F
-- Mathlib.Order.WithBot
WithTop.untop.eq_1 : ∀ {α : Type u_1} (x_2 : α) (x_3 : ↑x_2 ≠ ⊤), WithTop.untop (some x_2) x_3 = x_2
-- Mathlib.Topology.DiscreteSubset
isClosed_of_subset_discrete_closed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ t → IsDiscrete t → IsClosed t → IsClosed s
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.import.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.DFinsupp
LinearMap.dfinsuppSum_apply : ∀ {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {γ : ι → Type u_12} [inst_6 : DecidableEq ι] [inst_7 : (i : ι) → Zero (γ i)]
  [inst_8 : (i : ι) → (x : γ i) → Decidable (x ≠ 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂) (b : M),
  (t.sum g) b = t.sum fun i d => (g i d) b
-- Mathlib.Topology.Algebra.Group.Defs
/-- A topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  -/
IsTopologicalAddGroup : (G : Type u) → [TopologicalSpace G] → [AddGroup G] → Prop
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.empty_sub_empty : ∀ {α : Type u_1} [inst : Sub α] (v w : Fin 0 → α), v - w = ![]
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- Give a bound on `‖(1 + t * z)⁻¹‖` for `0 ≤ t ≤ 1` and `‖z‖ < 1`.  -/
Complex.norm_one_add_mul_inv_le : ∀ {t : ℝ}, t ∈ Set.Icc 0 1 → ∀ {z : ℂ}, ‖z‖ < 1 → ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
-- Mathlib.Algebra.Category.Ring.FilteredColimits
RingCat.FilteredColimits.forget₂SemiRing_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ RingCat SemiRingCat)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S], Module.FinitePresentation S Ω[S⁄R]
-- Mathlib.Probability.Moments.CovarianceBilin
/-- Covariance of a measure on an inner product space, as a continuous bilinear form.  -/
ProbabilityTheory.covarianceBilin : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [inst_2 : MeasurableSpace E] → [BorelSpace E] → MeasureTheory.Measure E → E →L[ℝ] E →L[ℝ] ℝ
-- Init.Data.Ord.Basic
List.compare_nil_left_eq_eq : ∀ {α : Type u_1} [inst : Ord α] {xs : List α}, compare [] xs = Ordering.eq ↔ xs = []
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If twice the oriented angles between two triples of points are equal, one triple is collinear
if and only if the other is.  -/
EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆ →
    (Collinear ℝ {p₁, p₂, p₃} ↔ Collinear ℝ {p₄, p₅, p₆})
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edges_eq_map_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.edges = List.map SimpleGraph.Dart.edge p.darts
-- Mathlib.NumberTheory.LucasLehmer
/-- The recurrence `s (i+1) = ((s i)^2 - 2) % (2^p - 1)` in `ℤ`.  -/
LucasLehmer.sMod : ℕ → ℕ → ℤ
-- Mathlib.RingTheory.Regular.IsSMulRegular
smul_top_inf_eq_smul_of_isSMulRegular_on_quot : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
  {r : R}, IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.Normal.hcongr_3 : ∀ (G G' : Type u_1),
  G = G' →
    ∀ (inst : Group G) (inst' : Group G'),
      inst ≍ inst' → ∀ (H : Subgroup G) (H' : Subgroup G'), H ≍ H' → H.Normal ≍ H'.Normal
-- Mathlib.Topology.ContinuousMap.Defs
/-- Coercion to a `ContinuousMap` is injective.

The unprimed version `ContinuousMap.coe_injective`
is used for the coercion from `C(X, Y)` to `X → Y`.  -/
ContinuousMap.coe_injective' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Type u_3}
  [inst_2 : FunLike F X Y] [inst_3 : ContinuousMapClass F X Y], Function.Injective toContinuousMap
-- Mathlib.Data.Multiset.Basic
/-- The strong induction principle for multisets.  -/
Multiset.strongInductionOn : {α : Type u_1} →
  {p : Multiset α → Sort u_3} → (s : Multiset α) → ((s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s) → p s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sin_mul_sum_sin : ∀ (n : ℕ) (a b : ℂ),
  Complex.sin (a / 2) * ∑ i ∈ Finset.range n, Complex.sin (a * ↑i + b) =
    Complex.sin (↑n * a / 2) * Complex.sin ((↑n - 1) * a / 2 + b)
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `upperSemicontinuousOn_iff_limsup_le`. -/
UpperSemicontinuousOn.limsup_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  UpperSemicontinuousOn f s → ∀ x ∈ s, Filter.limsup f (nhdsWithin x s) ≤ f x
-- Init.Data.UInt.Bitwise
UInt16.or_assoc : ∀ (a b c : UInt16), a ||| b ||| c = a ||| (b ||| c)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.lcm_zero_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x : R), EuclideanDomain.lcm 0 x = 0
-- Mathlib.Order.DirSupClosed
dirSupClosedOn_iff_of_linearOrder : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : LinearOrder α],
  DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
-- Init.Data.Vector.Lemmas
Vector.contains_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {x : α}, xs.toArray.contains x = xs.contains x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.RankFunction.isRegular : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] [WellFoundedLT α] [h.IsProper]
  (f : h.RankFunction α), h.IsRegular
-- Mathlib.RingTheory.Localization.Away.Basic
Localization.awayMap_surjective_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] {f : R →+* S} {r : R},
  Function.Surjective ⇑(Localization.awayMap f r) ↔ ∀ (a : S), ∃ b m, f b = f r ^ m * a
-- Mathlib.Analysis.Asymptotics.Lemmas
Filter.IsBoundedUnder.isBigO_const : ∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] {f : α → E}
  {l : Filter α}, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f) → ∀ {c : F''}, c ≠ 0 → f =O[l] fun _x => c
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.lex_def : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop}
  {a b : Π₀ (i : ι), α i}, DFinsupp.Lex r s a b ↔ ∃ j, (∀ (d : ι), r d j → a d = b d) ∧ s j (a j) (b j)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] → [inst_2 : NonAssocSemiring β] → [inst_3 : Preorder β] → FunLike (α →+*o β) α β
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- If `v` is a nonnegative function, then the Gauss norm is nonnegative.  -/
Polynomial.gaussNorm_nonneg : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R)
  [NonnegHomClass F R ℝ], 0 ≤ c → 0 ≤ Polynomial.gaussNorm v c p
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- The following square commutes:
```
Proj ℬ         ⟶ Proj 𝒜₁
    ^                   ^
    |                   |
Spec A₂[f(s)⁻¹]₀ ⟶ Spec A₁[s⁻¹]₀
```
 -/
AlgebraicGeometry.Proj.awayι_comp_map_assoc : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} (hi : 0 < i)
  (s : A) (hs : s ∈ 𝒜 i) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj 𝒜 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι ℬ (f s) ⋯ hi)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.map f hf) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.map f s)))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 s hs hi) h)
-- Mathlib.RingTheory.Localization.Module
LocalizedModule.map_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {N : Type u_3} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (l : M →ₗ[R] N),
  Function.Surjective ⇑l → Function.Surjective ⇑((LocalizedModule.map S) l)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- If two words have a common maximal reduction, then they correspond to the same element in the
free group.  -/
FreeGroup.reduce.exact : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.reduce L₁ = FreeGroup.reduce L₂ → FreeGroup.mk L₁ = FreeGroup.mk L₂
-- Lean.MetavarContext
Lean.DelayedMetavarAssignment.mk.sizeOf_spec : ∀ (fvars : Array Lean.Expr) (mvarIdPending : Lean.MVarId),
  sizeOf { fvars := fvars, mvarIdPending := mvarIdPending } = 1 + sizeOf fvars + sizeOf mvarIdPending
-- Mathlib.Analysis.Asymptotics.Defs
Filter.EventuallyEq.isBigO : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {l : Filter α} {f₁ f₂ : α → E}, f₁ =ᶠ[l] f₂ → f₁ =O[l] f₂
-- Lean.Elab.Term.TermElabM
/-- Refer to the given term elaborator by a scoped `Syntax` object.  -/
Lean.Elab.Term.elabToSyntax : {α : Type} →
  Lean.Elab.Term.FixedTermElab →
    (Lean.Term → Lean.Elab.TermElabM α) →
      optParam (Option Lean.MessageData) none → optParam Lean.Syntax Lean.Syntax.missing → Lean.Elab.TermElabM α
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (y : Y), IsLocallyConstant (Function.const X y)
-- Mathlib.Data.ENat.Lattice
ENat.iSup_zero : ∀ {ι : Sort u_1}, ⨆ x, 0 = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsConj.ext : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ}
  {σ₁ σ₂ : Gal(K/k)}, NumberField.ComplexEmbedding.IsConj φ σ₁ → NumberField.ComplexEmbedding.IsConj φ σ₂ → σ₁ = σ₂
-- Mathlib.Algebra.Order.Module.Defs
smul_nonneg : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulMono α β], 0 ≤ a → 0 ≤ b₁ → 0 ≤ a • b₁
-- Mathlib.Algebra.Order.Group.PosPart
/-- **Alias** of the reverse direction of `leOnePart_eq_inv`. -/
leOnePart_of_le_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], a ≤ 1 → a⁻ᵐ = a⁻¹
-- Std.Data.DTreeMap.Internal.Def
/-- The size information stored in the tree.  -/
Std.DTreeMap.Internal.Impl.size : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ℕ
-- Mathlib.Data.Multiset.Count
Multiset.le_iff_count : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ≤ t ↔ ∀ (a : α), Multiset.count a s ≤ Multiset.count a t
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.ext : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {U V : OpenSubgroup G},
  (∀ (x : G), x ∈ U ↔ x ∈ V) → U = V
-- Mathlib.Data.Finsupp.Defs
Finsupp.ofSupportFinite_coe : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α → M} {hf : (Function.support f).Finite},
  ⇑(Finsupp.ofSupportFinite f hf) = f
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.coe_toLinearMap : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (h : f v = 0), ↑(LinearEquiv.transvection h) = LinearMap.transvection f v
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.map_map : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (S : Subalgebra R A) (g : B →ₐ[R] C) (f : A →ₐ[R] B),
  Subalgebra.map g (Subalgebra.map f S) = Subalgebra.map (g.comp f) S
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRup : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    ∀ (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
      (f.insertRupUnits units).1.clearRupUnits = f
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.norm_fourier_apply_le_toLp_one : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] (f : SchwartzMap V F) (x : V),
  ‖(FourierTransform.fourier f) x‖ ≤ ‖f.toLp 1 MeasureTheory.volume‖
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι} (c : f.Cell j),
  CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex (f.b j) = c.mapToSucc
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapDerivedCategorySingleFunctor.eq_1 : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.Abelian C₁]
  [inst_2 : HasDerivedCategory C₁] {C₂ : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂]
  [inst_4 : CategoryTheory.Abelian C₂] [inst_5 : HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂)
  [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] (n : ℤ),
  F.mapDerivedCategorySingleFunctor n =
    CategoryTheory.Functor.isoWhiskerRight (DerivedCategory.singleFunctorIsoCompQ C₁ n) F.mapDerivedCategory ≪≫
      (CochainComplex.singleFunctor C₁ n).associator DerivedCategory.Q F.mapDerivedCategory ≪≫
        (CochainComplex.singleFunctor C₁ n).isoWhiskerLeft F.mapDerivedCategoryFactors ≪≫
          ((CochainComplex.singleFunctor C₁ n).associator (F.mapHomologicalComplex (ComplexShape.up ℤ))
                DerivedCategory.Q).symm ≪≫
            CategoryTheory.Functor.isoWhiskerRight
                (HomologicalComplex.singleMapHomologicalComplex F (ComplexShape.up ℤ) n) DerivedCategory.Q ≪≫
              F.associator (HomologicalComplex.single C₂ (ComplexShape.up ℤ) n) DerivedCategory.Q ≪≫
                (F.isoWhiskerLeft (DerivedCategory.singleFunctorIsoCompQ C₂ n)).symm
-- Init.Data.UInt.Lemmas
USize.toNat_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < USize.size → (USize.ofNatClamp n).toNat = n
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_left_le_mk_mul_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk (a * b) ↔ MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b
-- Mathlib.Algebra.Homology.CommSq
/-- A commutative square in a preadditive category is a pushout square iff
the corresponding diagram `X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0` makes `X₄` a cokernel.  -/
CategoryTheory.CommSq.isColimitEquivIsColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X₁ X₂ X₃ X₄ : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] →
          {f : X₁ ⟶ X₂} →
            {g : X₁ ⟶ X₃} →
              {inl : X₂ ⟶ X₄} →
                {inr : X₃ ⟶ X₄} →
                  (sq : CategoryTheory.CommSq f g inl inr) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯) ≃
                      CategoryTheory.Limits.IsColimit sq.cokernelCofork
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (I J : CategoryTheory.InjectiveResolution X) {Z : CochainComplex C ℕ} (h : I.cocomplex ⟶ Z),
  CategoryTheory.CategoryStruct.comp J.ι (CategoryTheory.CategoryStruct.comp (I.homotopyEquiv J).inv h) =
    CategoryTheory.CategoryStruct.comp I.ι h
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
/-- A finite measure `μ` over `(Π i, X i) × (Π j, Y j)` is determined by the values
`∫ p, (Π i, f i (p.1 i)) * (Π j, g j (p.2 j)) ∂μ`, for `f : (i : ι) → X i → ℝ`
and `g : (j : κ) → Y j → ℝ` any families of bounded continuous functions.  -/
Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction : ∀ {ι : Type u_1} {κ : Type u_2} {X : ι → Type u_5} {Y : κ → Type u_6} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mY : (j : κ) → MeasurableSpace (Y j)} [inst_3 : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)]
  [∀ (j : κ), HasOuterApproxClosed (Y j)] [inst_6 : Fintype ι] [inst_7 : Fintype κ]
  {μ ν : MeasureTheory.Measure (((i : ι) → X i) × ((j : κ) → Y j))} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : (j : κ) → BoundedContinuousFunction (Y j) ℝ),
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂μ =
        ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), (∏ i, (f i) (p.1 i)) * ∏ j, (g j) (p.2 j) ∂ν) →
    μ = ν
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- The composition of two open immersions is an open immersion.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] {Z : AlgebraicGeometry.PresheafedSpace C} (g : Y ⟶ Z)
  [hg : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion g],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Field.Basic
div_add_div : ∀ {K : Type u_1} [inst : Semifield K] {b d : K} (a c : K), b ≠ 0 → d ≠ 0 → a / b + c / d = (a * d + b * c) / (b * d)
-- Mathlib.Analysis.InnerProductSpace.Continuous
Dense.eq_zero_of_inner_right : ∀ {E : Type u_4} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E} {S : Set E}, Dense S → (∀ v ∈ S, inner 𝕜 v x = 0) → x = 0
-- Mathlib.Tactic.FunProp.Types
/-- Increase heartbeat, throws error when `maxSteps` was reached  -/
Mathlib.Meta.FunProp.increaseSteps : Mathlib.Meta.FunProp.FunPropM Unit
-- Mathlib.Algebra.Free
Magma.AssocQuotient.lift_of : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Semigroup β] (f : α →ₙ* β) (x : α),
  (Magma.AssocQuotient.lift f) (Magma.AssocQuotient.of x) = f x
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.tensor.injEq : ∀ {C : Type u} (a : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a_1 : C)
  (a_2 : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) (a_3 : C),
  (a.tensor a_1 = a_2.tensor a_3) = (a = a_2 ∧ a_1 = a_3)
-- Lean.Parser.Tactic.Doc
/-- Find all alternatives for a given canonical tactic name.
 -/
Lean.Parser.Tactic.Doc.aliases : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Lean.NameSet
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_9.splitter : (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
  (motive : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig → Sort u_1) →
    (input : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig) →
      ((pred : Std.Tactic.BVDecide.BVPred) →
          (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) → motive { val := pred, cache := cache }) →
        motive input
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkInit : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ne_int : ∀ {x : ℝ}, Irrational x → ∀ (m : ℤ), x ≠ ↑m
-- Mathlib.Data.Finset.NAry
Finset.image₂_singleton_inter : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {a : α} [inst_1 : DecidableEq β]
  (t₁ t₂ : Finset β),
  Function.Injective (f a) → Finset.image₂ f {a} (t₁ ∩ t₂) = Finset.image₂ f {a} t₁ ∩ Finset.image₂ f {a} t₂
-- Init.Data.UInt.Bitwise
USize.not_eq_neg_sub : ∀ (a : USize), ~~~a = -a - 1