mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Length
Module.length_eq_of_surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra S R] [inst_5 : Module S M] [IsScalarTower S R M],
  Function.Surjective ⇑(algebraMap S R) → Module.length S M = Module.length R M
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₀.eq_1 : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] (eA : A ≌ A')
  (e' : A' ≌ B'), AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e' = eA.trans e'
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_mul : ∀ {α : Type u_1} (a b : FreeMonoid α), (a * b).length = a.length + b.length
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasInitial C]
  {c : CategoryTheory.Limits.BinaryCofan X Y},
  CategoryTheory.IsVanKampenColimit c →
    CategoryTheory.IsPullback
      (CategoryTheory.Limits.initial.to
        ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }))
      (CategoryTheory.Limits.initial.to
        ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
      c.inl c.inr
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticOnNhd : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_5} {Em : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (Em i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em F)
  {s : Set ((i : ι) → Em i)}, AnalyticOnNhd 𝕜 (⇑f) s
-- Std.Time.Format.Modifier
Std.Time.Modifier.Q.inj : ∀ {presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text},
  Std.Time.Modifier.Q presentation = Std.Time.Modifier.Q presentation_1 → presentation = presentation_1
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `ε₀` is the first fixed point of `ω ^ ⬝`, i.e. the supremum of `ω`, `ω ^ ω`, `ω ^ ω ^ ω`, … 

Conventions for notations in identifiers:

 * The recommended spelling of `ε₀` in identifiers is `epsilon_zero`. -/
Ordinal.termε₀ : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle between three points equals minus the unoriented angle if the sign is
negative.  -/
EuclideanGeometry.oangle_eq_neg_angle_of_sign_eq_neg_one : ∀ {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},
  (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1 →
    EuclideanGeometry.oangle p₁ p₂ p₃ = -↑(EuclideanGeometry.angle p₁ p₂ p₃)
-- Mathlib.Analysis.Normed.Ring.Units
/-- The group of units of a normed ring with summable geometric series is an open subset
of the ring.  -/
Units.isOpen : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R], IsOpen {x | IsUnit x}
-- Mathlib.Data.Real.Basic
/-- A ring homomorphism `f : α →+* β` is bounded with respect to the functions `nα : α → ℝ` and
`nβ : β → ℝ` if there exists a positive constant `C` such that for all `x` in `α`,
`nβ (f x) ≤ C * nα x`.  -/
RingHom.IsBoundedWrt : {α : Type u_1} → [inst : Ring α] → {β : Type u_2} → [inst_1 : Ring β] → (α → ℝ) → (β → ℝ) → (α →+* β) → Prop
-- Init.Data.Array.Basic
/-- Returns `true` if the monadic predicate `p` returns `true` for any element of `as`.

Short-circuits upon encountering the first `true`. The elements in `as` are examined in order from
left to right.

The optional parameters `start` and `stop` control the region of the array to be checked. Only the
elements with indices from `start` (inclusive) to `stop` (exclusive) are checked. By default, the
entire array is checked.
 -/
Array.anyM : {α : Type u} →
  {m : Type → Type w} → [Monad m] → (α → m Bool) → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m Bool
-- Mathlib.Topology.Compactness.SigmaCompact
CompactSpace.sigmaCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X], SigmaCompactSpace X
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A space is totally disconnected iff its connected components are subsingletons.  -/
totallyDisconnectedSpace_iff_connectedComponent_subsingleton : ∀ {α : Type u} [inst : TopologicalSpace α], TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton
-- Mathlib.RingTheory.Congruence.Basic
RingCon.ringConGen_sup : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (r s : R → R → Prop), ringConGen (r ⊔ s) = ringConGen r ⊔ ringConGen s
-- Init.Data.List.Range
List.getLast?_range : ∀ {n : ℕ}, (List.range n).getLast? = if n = 0 then none else some (n - 1)
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.alias.injEq : ∀ (p p_1 : Lean.Parser.ParserAliasValue),
  (Lean.Parser.ParserResolution.alias p = Lean.Parser.ParserResolution.alias p_1) = (p = p_1)
-- Mathlib.Topology.Algebra.Monoid
le_nhds_mul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] (a b : M),
  nhds a * nhds b ≤ nhds (a * b)
-- Mathlib.Probability.Distributions.Gaussian.CharFun
/-- The measure `μ` is Gaussian if and only if there
exist `m : E` and `f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ`
satisfying `f.toBilinForm.IsPosSemidef` and `charFunDual μ L = exp (L m * I - f L L / 2)`.  -/
ProbabilityTheory.isGaussian_iff_gaussian_charFunDual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : NormedSpace ℝ E]
  [MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.IsGaussian μ ↔
    ∃ m f,
      f.toBilinForm.IsPosSemidef ∧
        ∀ (L : StrongDual ℝ E), MeasureTheory.charFunDual μ L = Complex.exp (↑(L m) * Complex.I - ↑((f L) L) / 2)
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Multiset.iSup_mem_map_of_exists_sSup_empty_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Multiset ι} (f : ι → α),
  (∃ x ∈ s, sSup ∅ ≤ f x) → ⨆ x ∈ s, f x ∈ Multiset.map f s
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_pow_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : Monoid Z] [inst_4 : ContinuousMul Z] (f : C(X × Y, Z)) (n : ℕ) (x : X),
  (f ^ n).curry x = f.curry x ^ n
-- Mathlib.Data.NNReal.Basic
NNReal.mul_iInf : ∀ {ι : Sort u_3} (f : ι → NNReal) (a : NNReal), a * iInf f = ⨅ i, a * f i
-- Lean.Expr
/-- Annotate `e` with `pp.piBinderTypes := flag`
The delaborator uses `pp` options.
 -/
Lean.Expr.setPPPiBinderTypes : Lean.Expr → Bool → Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.IsCompl.adjMatrix_add_adjMatrix_eq_adjMatrix_completeGraph : ∀ (α : Type u_1) {V : Type u_2} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : AddZeroClass α] [inst_3 : One α] {H : SimpleGraph V} [inst_4 : DecidableRel H.Adj],
  IsCompl G H →
    SimpleGraph.adjMatrix α G + SimpleGraph.adjMatrix α H = SimpleGraph.adjMatrix α (SimpleGraph.completeGraph V)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.splitAtPred.match_3.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.symm.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (cme : M ≃ₜ* N), cme.symm = { toMulEquiv := cme.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false)
  {h : k ∈ m.insertMany l}, (m.insertMany l)[k] = m[k]
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} [inst_1 : Inhabited (γ k)],
  t.WF → (Std.DTreeMap.Raw.filterMap f t).get! k = ((t.get? k).bind (f k)).get!
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedLocalTimeType : Inhabited Std.Time.TimeZone.TZif.LocalTimeType
-- Init.Data.Order.Ord
Option.instReflOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.ReflOrd α], Std.ReflOrd (Option α)
-- Mathlib.Data.List.Sort
/-- If `c` is a sorted sublist of `l`, then `c` is still a sublist of `insertionSort r l`.
 -/
List.sublist_insertionSort : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] {l c : List α},
  List.Pairwise r c → c.Sublist l → c.Sublist (List.insertionSort r l)
-- Mathlib.Data.UInt
/-- Is this a lowercase ASCII letter?  -/
UInt8.isASCIILower : UInt8 → Bool
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL.eq_1 : ∀ {𝕜 : 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 →L[𝕜] F) (g : G →L[𝕜] H),
  TensorProduct.mapL f g = ContinuousLinearMap.rTensor H f ∘SL ContinuousLinearMap.lTensor E g
-- Mathlib.Order.Antichain
isChain_and_isAntichain_iff_subsingleton : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsChain r s ∧ IsAntichain r s ↔ s.Subsingleton
-- Mathlib.Data.Nat.Squarefree
Nat.primeFactors_prod_primeFactors : ∀ (n : ℕ), (∏ p ∈ n.primeFactors, p).primeFactors = n.primeFactors
-- Init.Data.UInt.Lemmas
USize.ofNat_eq_iff_mod_eq_toNat : ∀ (a : ℕ) (b : USize), USize.ofNat a = b ↔ a % 2 ^ System.Platform.numBits = b.toNat
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.linearIsometryEquiv_mk' : ∀ {𝕜 : Type u_1} {V₁ : Type u_3} {V₂ : Type u_5} {P₁ : Type u_8} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁] [inst_2 : NormedSpace 𝕜 V₁] [inst_3 : PseudoMetricSpace P₁]
  [inst_4 : NormedAddTorsor V₁ P₁] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p : P₁)
  (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p), (AffineIsometryEquiv.mk' e e' p h).linearIsometryEquiv = e'
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.brecOn.go : {pu : Lean.Compiler.LCNF.Purity} →
  {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u} →
    {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} →
      {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u} →
        {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} →
          {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u} →
            {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} →
              (t : Lean.Compiler.LCNF.Cases pu) →
                ((t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t) →
                  ((t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t) →
                    ((t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t) →
                      ((t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t) →
                        ((t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t) →
                          ((t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t) →
                            motive_3 t ×' t.below
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- An affine isometric equivalence between two normed vector spaces,
denoted `f : P ≃ᵃⁱ[𝕜] P₂`.  -/
AffineIsometryEquiv : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      (P : Type u_10) →
        (P₂ : Type u_11) →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [NormedSpace 𝕜 V₂] →
                        [inst : PseudoMetricSpace P₂] →
                          [NormedAddTorsor V₂ P₂] → Type (max (max (max u_10 u_11) u_2) u_5)
-- Mathlib.RingTheory.Morita.Matrix
/-- Moreover `ModuleCat.matrixEquivalence` is a `MoritaEquivalence`.  -/
moritaEquivalenceMatrix : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          (R₀ : Type u_1) → [inst_3 : CommRing R₀] → [inst_4 : Algebra R₀ R] → ι → MoritaEquivalence R₀ R (Matrix ι ι R)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- A continuous affine equivalence, denoted `P₁ ≃ᴬ[k] P₂`, between two affine topological spaces
is an affine equivalence such that forward and inverse maps are continuous.  -/
«term_≃ᴬ[_]_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The formula `ψ(P₁ + P₂) = (ψ(P₂)(x(P₁) - x(P₃)) - ψ(P₁)(x(P₂) - x(P₃))) / (x(P₂) - x(P₁))`,
where `ψ(x,y) = 2y + a₁x + a₃`.  -/
WeierstrassCurve.Affine.addY_sub_negY_addY : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ : F} (y₁ y₂ : F),
  x₁ ≠ x₂ →
    have x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
    have y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂);
    y₃ - W.negY x₃ y₃ = ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (x₂ - x₁)
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateIsoEquiv_apply_inv : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : L₂ ≅ L₁), ((CategoryTheory.conjugateIsoEquiv adj₁ adj₂) α).inv = (CategoryTheory.conjugateEquiv adj₂ adj₁) α.inv
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaEquiv_symm_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
  {F : CategoryTheory.Functor C (Type v₁)} (t : F.obj X),
  CategoryTheory.coyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map f.op) (CategoryTheory.coyonedaEquiv.symm t)
-- Init.Data.SInt.Lemmas
Int8.toInt_ofBitVec : ∀ (b : BitVec 8), (Int8.ofBitVec b).toInt = b.toInt
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidal.eq_1 : ∀ (M : Type u) [inst : AddMonoid M],
  CategoryTheory.Discrete.addMonoidal M =
    { tensorObj := fun X Y => { as := X.as + Y.as }, whiskerLeft := fun X x x_1 f => CategoryTheory.eqToHom ⋯,
      whiskerRight := fun {X₁ X₂} f X => CategoryTheory.eqToHom ⋯,
      tensorHom := fun {X₁ Y₁ X₂ Y₂} f g => CategoryTheory.eqToHom ⋯, tensorUnit := { as := 0 },
      associator := fun x x_1 x_2 => CategoryTheory.Discrete.eqToIso ⋯,
      leftUnitor := fun X => CategoryTheory.Discrete.eqToIso ⋯,
      rightUnitor := fun X => CategoryTheory.Discrete.eqToIso ⋯, tensorHom_def := ⋯, id_tensorHom_id := ⋯,
      tensorHom_comp_tensorHom := ⋯, whiskerLeft_id := ⋯, id_whiskerRight := ⋯, associator_naturality := ⋯,
      leftUnitor_naturality := ⋯, rightUnitor_naturality := ⋯, pentagon := ⋯, triangle := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of the reverse direction of `one_le_inv₀`. -/
Bound.one_le_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → a ≤ 1 → 1 ≤ a⁻¹
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instIdemCommSemiring : {X : AlgebraicGeometry.Scheme} → IdemCommSemiring X.IdealSheafData
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_zero_right : ∀ {p t : ℝ}, p.rpowIntegrand₀₁ t 0 = 0
-- Init.Data.SInt.Lemmas
ISize.add_left_inj : ∀ {a b : ISize} (c : ISize), a + c = b + c ↔ a = b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {f : Option β → Option β} {hc : k ∈ t.alter k f}, (t.alter k f)[k] = (f t[k]?).get ⋯
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_closedBall_center : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (x : E) (r : ℝ), μ (Metric.closedBall x r) = μ (Metric.closedBall 0 r)
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_neg_neg_pos_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ},
  ↑(A ^ 3).card ≤ K * ↑A.card → ↑(A⁻¹ * A⁻¹ * A).card ≤ K ^ 2 * ↑A.card
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
/-- Construct the equivalence class `[f]` of an integrable function `f`, as a member of the
space `Lp β 1 μ`.  -/
MeasureTheory.Integrable.toL1 : {α : Type u_1} →
  {β : Type u_2} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        [inst : NormedAddCommGroup β] → (f : α → β) → MeasureTheory.Integrable f μ → ↥(MeasureTheory.Lp β 1 μ)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instInhabitedTacticParsedSnapshot.default : Lean.Elab.Tactic.TacticParsedSnapshot
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.instGroupSubtypeMemSubmonoid : {M : Type u_1} → [inst : Monoid M] → Group ↥(IsUnit.submonoid M)
-- Mathlib.Topology.CWComplex.Classical.Graph
Topology.CWComplex.vertexSet_OneSkeletonGraph : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [inst_1 : Topology.CWComplex C],
  (Topology.CWComplex.OneSkeletonGraph C).vertexSet = Set.univ
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (s₁ s₂ : Lean.Grind.AC.Seq)
  (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₂))
  (x₁ x₂ : Lean.Grind.AC.Var),
  s₁ = Lean.Grind.AC.Seq.var x₁ →
    s₂ = Lean.Grind.AC.Seq.var x₂ →
      (match s₁, s₂ 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₂
-- Init.Data.BitVec.Lemmas
BitVec.slt_iff_toInt_lt : ∀ {w : ℕ} {x y : BitVec w}, x.slt y = true ↔ x.toInt < y.toInt
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} {hf : F.relativelyRepresentable f} {a : C} {g : F.obj a ⟶ Y}
  [F.Faithful] {c : C} {a_1 b : c ⟶ hf.pullback g},
  a_1 = b ↔
    CategoryTheory.CategoryStruct.comp (F.map a_1) (hf.fst g) =
        CategoryTheory.CategoryStruct.comp (F.map b) (hf.fst g) ∧
      CategoryTheory.CategoryStruct.comp a_1 (hf.snd g) = CategoryTheory.CategoryStruct.comp b (hf.snd g)
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialAt.analyticWithinAt : ∀ {𝕜 : 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] {f : E → F} {x : E} {s : Set E},
  CPolynomialAt 𝕜 f x → AnalyticWithinAt 𝕜 f s x
-- Mathlib.Algebra.GroupWithZero.Defs
MulDivCancelClass.mul_div_cancel : ∀ {M₀ : Type u_2} {inst : MonoidWithZero M₀} {inst_1 : Div M₀} [self : MulDivCancelClass M₀] (a b : M₀),
  b ≠ 0 → a * b / b = a
-- Init.Data.Slice.List.Lemmas
ListSlice.size_mkSlice_rcc : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.size (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = min (hi + 1) (Std.Slice.size xs) - lo
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- Pullbacks distribute over universal coproducts on the right: This is the isomorphism
`∐ (Xᵢ ×[S] B) ≅ (∐ Xᵢ) ×[S] B`.  -/
CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) (s : (i : ι) → CategoryTheory.Limits.PullbackCone (f i) v)
      (hs : (i : ι) → CategoryTheory.Limits.IsLimit (s i)) (t : CategoryTheory.Limits.PullbackCone u v)
      (ht : CategoryTheory.Limits.IsLimit t) (d : CategoryTheory.Limits.Cofan fun i => (s i).pt) (e : d.pt ≅ t.pt),
      autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
          CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right._auto_1 →
        autoParam
            (∀ (i : ι),
              CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom t.fst) =
                CategoryTheory.CategoryStruct.comp (s i).fst (a.inj i))
            CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right._auto_3 →
          autoParam
              (∀ (i : ι),
                CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom t.snd) =
                  (s i).snd)
              CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right._auto_5 →
            Nonempty (CategoryTheory.Limits.IsColimit d)
-- Init.Data.Float.Float32
instDecidableEqFloat32.decEq : (x x_1 : Float32) → Decidable (x = x_1)
-- Mathlib.Analysis.Normed.Ring.Units
/-- The formula `Ring.inverse (x + t) = Ring.inverse (1 + x⁻¹ * t) * x⁻¹` holds for `t` sufficiently
small.  -/
NormedRing.inverse_add : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ),
  ∀ᶠ (t : R) in nhds 0, Ring.inverse (↑x + t) = Ring.inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instDistrib : {R : Type u_1} → [Distrib R] → Distrib Rᵐᵒᵖ
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
/-- Tensor products distribute over a direct sum on the right.  -/
TensorProduct.directSumRight : (R : Type u) →
  [inst : CommSemiring R] →
    (S : Type u_1) →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {ι₂ : Type v₂} →
            [DecidableEq ι₂] →
              (M₁' : Type w₁') →
                (M₂ : ι₂ → Type w₂) →
                  [inst_4 : AddCommMonoid M₁'] →
                    [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] →
                      [inst_6 : Module R M₁'] →
                        [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)] →
                          [inst_8 : Module S M₁'] →
                            [inst_9 : IsScalarTower R S M₁'] →
                              TensorProduct R M₁' (DirectSum ι₂ fun i => M₂ i) ≃ₗ[S]
                                DirectSum ι₂ fun i => TensorProduct R M₁' (M₂ i)