mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_eq_default : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.contains a = false → m.get! a = default
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SymExtension.getStateCore : {σ : Type} → Lean.Meta.Sym.SymExtension σ → Array Lean.Meta.Sym.SymExtensionState → IO σ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.nonsingular_submatrix_equiv_iff : ∀ {n : Type u_1} {m : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommSemiring R] {A : Matrix n n R} {e₁ e₂ : m ≃ n},
  (A.submatrix ⇑e₁ ⇑e₂).Nonsingular ↔ A.Nonsingular
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) (f : σ → MvPolynomial τ R)
  (φ : MvPolynomial σ R),
  (MvPolynomial.expand p) ((MvPolynomial.bind₁ f) φ) = (MvPolynomial.bind₁ fun i => (MvPolynomial.expand p) (f i)) φ
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_congr : ∀ {α : Type u} {β : Type v} (e : α ≃ β), Cardinal.toNat (Cardinal.mk α) = Cardinal.toNat (Cardinal.mk β)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_neg : ∀ {R : Type u_1} {a b : R} [inst : NegZeroClass R] (x : R), QuadraticAlgebra.C (-x) = -QuadraticAlgebra.C x
-- Mathlib.Order.Interval.Finset.Nat
Nat.image_sub_const_Ico : ∀ {a b c : ℕ}, c ≤ a → Finset.image (fun x => x - c) (Finset.Ico a b) = Finset.Ico (a - c) (b - c)
-- Mathlib.LinearAlgebra.Span.Basic
/-- The inclusion of an `R`-submodule into its `S`-span, as an `R`-linear map.  -/
Submodule.inclusionSpan : {R : Type u_1} →
  {M : Type u_4} →
    (S : Type u_7) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring S] →
              [inst_4 : SMul R S] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] → (p : Submodule R M) → ↥p →ₗ[R] ↥(Submodule.span S ↑p)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.find?_insert_self : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {c : RBTree.RBColor} {n : ℕ} {v : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut] {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.Ordered cmp t → cut v = Ordering.eq → RBTree.RBNode.find? cut (RBTree.RBNode.insert cmp t v) = some v
-- Mathlib.Algebra.Group.Defs
AddZero.toZero : {M : Type u_2} → [self : AddZero M] → Zero M
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.homeomorph_comp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X},
  IsEvenlyCovered f x I → ∀ {Y : Type u_4} [inst_3 : TopologicalSpace Y] (g : X ≃ₜ Y), IsEvenlyCovered (⇑g ∘ f) (g x) I
-- Mathlib.Algebra.Star.Unitary
Unitary.mapEquiv_trans : ∀ {R : Type u_2} {S : Type u_3} {T : Type u_4} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S]
  [inst_3 : StarMul S] [inst_4 : Monoid T] [inst_5 : StarMul T] (f : R ≃⋆* S) (g : S ≃⋆* T),
  Unitary.mapEquiv (f.trans g) = (Unitary.mapEquiv f).trans (Unitary.mapEquiv g)
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.GrothendieckTopology.toPrecoverage_top : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C], ⊤.toPrecoverage = ⊤
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.wasDeleted.sizeOf_spec : sizeOf Lean.Widget.DiffTag.wasDeleted = 1
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.withNotFirst : {α : Type} → Lean.Elab.Term.ToParserDescrM α → Lean.Elab.Term.ToParserDescrM α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_diff_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Mathlib.Analysis.RCLike.Basic
RCLike.instStarModuleReal : ∀ {K : Type u_1} [inst : RCLike K], StarModule ℝ K
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.boxProdRight.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) {H : SimpleGraph β} {b₁ b₂ : β} (a : α),
  SimpleGraph.Walk.boxProdRight G a = SimpleGraph.Walk.map (G.boxProdRight H a).toHom
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.trans_toPartialEquiv : ∀ {X : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : MulAction G X] (f g : Equidecomp X G),
  (f.trans g).toPartialEquiv = f.trans g.toPartialEquiv
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq.eq_def : ∀ (x x_1 : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.instBEqPoly.beq x x_1 =
    match x, x_1 with
    | Lean.Grind.Linarith.Poly.nil, Lean.Grind.Linarith.Poly.nil => true
    | Lean.Grind.Linarith.Poly.add a a_1 a_2, Lean.Grind.Linarith.Poly.add b b_1 b_2 =>
      a == b && (a_1 == b_1 && Lean.Grind.Linarith.instBEqPoly.beq a_2 b_2)
    | x, x_2 => false
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.mk.inj : ∀ {α : Type u_4} {inst : TopologicalSpace α} {toCompacts : TopologicalSpace.Compacts α}
  {interior_nonempty' : (interior toCompacts.carrier).Nonempty} {toCompacts_1 : TopologicalSpace.Compacts α}
  {interior_nonempty'_1 : (interior toCompacts_1.carrier).Nonempty},
  { toCompacts := toCompacts, interior_nonempty' := interior_nonempty' } =
      { toCompacts := toCompacts_1, interior_nonempty' := interior_nonempty'_1 } →
    toCompacts = toCompacts_1
-- Mathlib.NumberTheory.LSeries.ZMod
/-- For `1 < re s` the congruence L-function agrees with the sum of the Dirichlet series.  -/
ZMod.LFunction_eq_LSeries : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) {s : ℂ}, 1 < s.re → ZMod.LFunction Φ s = LSeries (fun x => Φ ↑x) s
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasStrictDerivAt.hasStrictFDerivAt_equiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {f' x : 𝕜},
  HasStrictDerivAt f f' x →
    ∀ (hf' : f' ≠ 0), HasStrictFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.insert k).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Init.Data.List.SplitOn.Lemmas
List.splitOnP_nil : ∀ {α : Type u_1} {p : α → Bool}, List.splitOnP p [] = [[]]
-- Mathlib.Algebra.Group.Prod
/-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `N`.  -/
MulHom.snd : (M : Type u_3) → (N : Type u_4) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] [inst_5 : SizeOf R]
  [inst_6 : SizeOf X] [inst_7 : SizeOf Y] (toFun : X → Y)
  (isAffineMap_toFun :
    autoParam (Convexity.IsAffineMap R toFun) Convexity.ConvexSpace.AffineMap.isAffineMap_toFun._autoParam),
  sizeOf { toFun := toFun, isAffineMap_toFun := isAffineMap_toFun } = 1 + sizeOf isAffineMap_toFun
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_div_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a / x) '' Set.Ici b = Set.Iic (a / b)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.neg_add_cancel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a : X ⟶ Y), -a + a = 0
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.sdiff_mem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {s t : Set ((i : ι) → α i)},
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α → s \ t ∈ MeasureTheory.measurableCylinders α
-- Mathlib.CategoryTheory.Subobject.Basic
/-- In fact, there's a type level bijection between the subobjects of isomorphic objects,
which preserves the order.  -/
CategoryTheory.Subobject.mapIsoToOrderIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (X ≅ Y) → CategoryTheory.Subobject X ≃o CategoryTheory.Subobject Y
-- Mathlib.Tactic.NormNum.BigOperators
/-- The set equals `a` inserted into the strict subset `s'`.  -/
Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons : {u : Lean.Level} →
  {α : Q(Type u)} →
    {s : Q(Multiset «$α»)} →
      (a : Q(«$α»)) → (s' : Q(Multiset «$α»)) → Q(«$s» = «$a» ::ₘ «$s'») → Mathlib.Meta.Multiset.ProveZeroOrConsResult s
-- Mathlib.Computability.Primrec.Basic
PrimrecPred.comp : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : β → Prop} {f : α → β},
  PrimrecPred p → Primrec f → PrimrecPred fun a => p (f a)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCancelCommMonoid : {α : Type u_1} → [AddCancelCommMonoid α] → AddCancelCommMonoid αᵒᵈ
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.property_liftInner : ∀ {α : Type u_1} {m : Type w → Type w'} {n : Type w → Type w''} [inst : MonadLiftT m n] {x : Std.Iterators.HetT m α},
  (Std.Iterators.HetT.liftInner n x).Property = x.Property
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- `α →ᵇ β` is the type of bounded continuous functions `α → β` from a topological space to a
metric space.

When possible, instead of parametrizing results over `(f : α →ᵇ β)`,
you should parametrize over `(F : Type*) [BoundedContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `BoundedContinuousMapClass`.  -/
BoundedContinuousFunction : (α : Type u) → (β : Type v) → [TopologicalSpace α] → [PseudoMetricSpace β] → Type (max u v)
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.inter₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size},
  m₁.WF → m₂.WF → (↑(Std.DHashMap.Internal.Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩)).WF
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.instIsEquivalenceOppositeFiniteEtaleFintypeCatFiberOfIsSepClosed : ∀ (Ω : Type u) [inst : Field Ω] [IsSepClosed Ω], (CommAlgCat.FiniteEtale.fiber Ω Ω).IsEquivalence
-- Mathlib.Algebra.Regular.SMul
/-- An element of `R` admitting a left inverse is `M`-regular.  -/
IsSMulRegular.of_mul_eq_one : ∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : Monoid R] [inst_1 : MulAction R M], a * b = 1 → IsSMulRegular M b
-- Mathlib.Topology.Neighborhoods
frequently_nhds_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {p : X → Prop},
  (∃ᶠ (y : X) in nhds x, p y) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ y ∈ U, p y
-- Init.Data.List.Basic
List.instLE : {α : Type u} → [LT α] → LE (List α)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_sup : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l₁ l₂ : Filter α} {f : α → E} {g : α → F},
  f =o[𝕜; l₁ ⊔ l₂] g ↔ f =o[𝕜; l₁] g ∧ f =o[𝕜; l₂] g
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.map_smul_right : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] [inst_13 : AddCommMonoid Q]
  [inst_14 : Module R Q] (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q),
  TensorProduct.AlgebraTensorModule.map f (r • g) = r • TensorProduct.AlgebraTensorModule.map f g
-- Mathlib.Data.Num.ZNum
Num.gcdAux.eq_1 : ∀ (x x_1 : Num), Num.gcdAux 0 x x_1 = x_1
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.center_prod : ∀ {M : Type u_1} [inst : MulOneClass M] {N : Type u_2} [inst_1 : MulOneClass N],
  Submonoid.center (M × N) = (Submonoid.center M).prod (Submonoid.center N)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 1-boundaries `B₁(G, A)` of `A : Rep k G`, defined as the image of the map
`(G² →₀ A) → (G →₀ A)` defined by `a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁`.  -/
groupHomology.boundaries₁ : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → Submodule k (G →₀ ↑A)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_hom_app_right : ∀ {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 Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).hom.app CategoryTheory.Limits.WalkingCospan.right =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Limits.cospan f g).comp F).obj CategoryTheory.Limits.WalkingCospan.right)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.limitsOfShape_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [W.IsStableUnderLimitsOfShape J], W.limitsOfShape J ≤ W
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceTo.eq_1 : ∀ (s : String.Slice) (pos : s.Pos),
  s.sliceTo pos =
    { str := s.str, startInclusive := s.startInclusive, endExclusive := pos.str, startInclusive_le_endExclusive := ⋯ }
-- Lean.Elab.Calc
Lean.Elab.Term.mkCalcStepViews : Lean.TSyntax `Lean.calcSteps → Lean.Elab.TermElabM (Array Lean.Elab.Term.CalcStepView)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A finite-dimensional `InnerProductSpace` has an orthonormal basis.  -/
stdOrthonormalBasis : (𝕜 : Type u_7) →
  [inst : RCLike 𝕜] →
    (E : Type u_8) →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → OrthonormalBasis (Fin (Module.finrank 𝕜 E)) 𝕜 E
-- Init.Prelude
/-- Constructs a synthetic `SourceInfo` using a `ref : Syntax` for the span.  -/
Lean.SourceInfo.fromRef : Lean.Syntax → optParam Bool false → Lean.SourceInfo
-- Mathlib.Analysis.Analytic.Constructions
AnalyticAtWithin.compContinuousLinearMap : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {u : E →L[𝕜] F} {f : F → G} {s : Set F} {x : E},
  AnalyticWithinAt 𝕜 f s (u x) → AnalyticWithinAt 𝕜 (f ∘ ⇑u) (⇑u ⁻¹' s) x
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (g : P →ₗ[R] Q)
  (f : N →ₗ[R] P), LinearMap.rTensor M (g ∘ₗ f) = LinearMap.rTensor M g ∘ₗ LinearMap.rTensor M f
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_asSigma : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C}
  (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y),
  CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl (CategoryTheory.Limits.FormalCoproduct.Hom.asSigma f).fst
      (CategoryTheory.Limits.FormalCoproduct.Hom.asSigma f).snd =
    f
-- Mathlib.Topology.Algebra.Monoid
Filter.Tendsto.val_inv_units : ∀ {ι : Type u_1} {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Monoid N] [inst_2 : ContinuousMul N]
  [inst_3 : T2Space N] {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [inst_4 : l.NeBot]
  (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂)),
  ↑(h₁.units h₂)⁻¹ = r₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {a : α}, a ∈ t → t.getKey? a = some (t.getKey! a)
-- Std.Http.Protocol.H1.Config
/-- Maximum number of bytes consumed while parsing one chunk-size line with extensions (default: 8192 bytes).
 -/
Std.Http.Protocol.H1.Config.maxChunkLineLength : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.LinearAlgebra.Span.TensorProduct
/-- If `A` is a flat epi `R`-algebra and `s` is a subset of an `A`-module `M` then the natural
surjection from `A ⊗[R] span R s` to `span A s` is an equivalence.  -/
Submodule.tensorSpanEquivSpan : (R : Type u_1) →
  (A : Type u_2) →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module A M] →
                  [IsScalarTower R A M] →
                    [Algebra.IsEpi R A] →
                      [Module.Flat R A] →
                        (s : Set M) → TensorProduct R A ↥(Submodule.span R s) ≃ₗ[A] ↥(Submodule.span A s)
-- Mathlib.Algebra.Divisibility.Basic
Dvd.intro : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- Given `h : F.IsEventuallyConstantTo i₀`, this is the (limit) cone for `F` whose
point is `F.obj i₀`.  -/
CategoryTheory.Functor.IsEventuallyConstantTo.cone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} → F.IsEventuallyConstantTo i₀ → [CategoryTheory.IsCofiltered J] → CategoryTheory.Limits.Cone F
-- Mathlib.Topology.UniformSpace.Basic
mem_uniformity_isClosed : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α}, s ∈ uniformity α → ∃ t ∈ uniformity α, IsClosed t ∧ t ⊆ s
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.instReprSimpCongrTheorems.repr : Lean.Meta.SimpCongrTheorems → ℕ → Std.Format
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mk.inj : ∀ {C : Type u} {as as_1 : C}, { as := as } = { as := as_1 } → as = as_1
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The associativity compatibility for the extension of scalars, in the exact form
that is needed in the definition `CommRingCat.moduleCatExtendScalarsPseudofunctor`
in the file `Mathlib/Algebra/Category/ModuleCat/Pseudofunctor.lean`  -/
ModuleCat.extendScalars_assoc' : ∀ {R₁ R₂ R₃ R₄ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : CommRing R₃] [inst_3 : CommRing R₄]
  (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (f₃₄ : R₃ →+* R₄),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsComp f₁₂ f₂₃).hom (ModuleCat.extendScalars f₃₄))
        (CategoryTheory.CategoryStruct.comp
          ((ModuleCat.extendScalars f₁₂).associator (ModuleCat.extendScalars f₂₃) (ModuleCat.extendScalars f₃₄)).hom
          (CategoryTheory.CategoryStruct.comp
            ((ModuleCat.extendScalars f₁₂).whiskerLeft (ModuleCat.extendScalarsComp f₂₃ f₃₄).inv)
            (ModuleCat.extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv))) =
    CategoryTheory.CategoryStruct.id (ModuleCat.extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_mulLeft₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MeasurableSpace G₀] [MeasurableMul G₀] {g : G₀},
  g ≠ 0 → MeasurableEmbedding fun x => g * x
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.continuousConstSMul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] {M : Type u_7} [inst_7 : Monoid M] [inst_8 : DistribMulAction M F]
  [inst_9 : SMulCommClass 𝕜₂ M F] [inst_10 : TopologicalSpace F] [inst_11 : IsTopologicalAddGroup F]
  [inst_12 : ContinuousConstSMul M F], ContinuousConstSMul M (E →SL[σ] F)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_sup_ker_eq_map : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L},
  LieIdeal.map f (I ⊔ f.ker) = LieIdeal.map f I
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.fvar : (decl : Qq.Impl.PatVarDecl) →
  have a := decl.fvarTy;
  Q(«$a»)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
/-- The ascending chain condition on principal ideals holds in a `WfDvdMonoid` domain.  -/
Ideal.setOfPred_isPrincipal_wellFoundedOn_gt : ∀ {α : Type u_1} [inst : CommSemiring α] [WfDvdMonoid α] [IsDomain α],
  {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.isUnsatEq.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Poly.num k))
  (h_2 : (x : Int.Internal.Linear.Poly) → motive x),
  (match Int.Internal.Linear.Poly.num k with
    | Int.Internal.Linear.Poly.num k => h_1 k
    | x => h_2 x) =
    h_1 k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableResolvableCompletionItemData.hash : Lean.Lsp.ResolvableCompletionItemData → UInt64
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isBoundary₁_of_mem_boundaries₁ : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ x ∈ groupHomology.boundaries₁ (Rep.ofDistribMulAction k G A), groupHomology.IsBoundary₁ x
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.ofReal_setAverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
  MeasureTheory.IntegrableOn f s μ →
    0 ≤ᵐ[μ.restrict s] f → ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hV2 : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] → [inst_1 : TopologicalSpace k] → [inst_2 : Monoid G] → (self : TopRep k G) → Module k ↑self
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.whisker_left.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c}
  (η : CategoryTheory.FreeBicategory.Hom₂ g h),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η) =
    1 + sizeOf a + sizeOf b + sizeOf c + sizeOf f + sizeOf g + sizeOf h + sizeOf η
-- Init.Data.UInt.Lemmas
UInt32.toFin_mul : ∀ (a b : UInt32), (a * b).toFin = a.toFin * b.toFin