mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- structure 2-isomorphism for composition of 1-morphisms  -/
CategoryTheory.StrictlyUnitaryPseudofunctorCore.mapComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) →
          {a b c : B} →
            (f : a ⟶ b) →
              (g : b ⟶ c) →
                self.map (CategoryTheory.CategoryStruct.comp f g) ≅
                  CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOn.neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {g : β → α} {s : Set β}, TendstoUniformlyOn f g l s → TendstoUniformlyOn (-f) (-g) l s
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomCompTriple.comp_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {x : R₁}, σ₂₃ (σ₁₂ x) = σ₁₃ x
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toSheafedSpace_map : ∀ {X Y : CommRingCatᵒᵖ} (f : X ⟶ Y),
  AlgebraicGeometry.Spec.toSheafedSpace.map f = AlgebraicGeometry.Spec.sheafedSpaceMap f.unop
-- Mathlib.Topology.UniformSpace.Basic
/-- Given `f : α → β` and a uniformity `u` on `β`, the inverse image of `u` under `f`
is the inverse image in the filter sense of the induced function `α × α → β × β`.
See note [reducible non-instances].  -/
UniformSpace.comap : {α : Type ua} → {β : Type ub} → (α → β) → UniformSpace β → UniformSpace α
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instAddCommGroup : {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} → AddCommGroup (M [⋀^ι]→ₗ[R] N')
-- Mathlib.Data.Real.Embedding
/-- Given `x` from `M`, one can informally write that, by transitivity,
`num / den ≤ x → x ≤ n → num / den ≤ n` for `den : ℕ` and `num n : ℕ`.
To avoid writing division for integer `num` and `den`, we express this in terms of
multiplication.  -/
num_le_nat_mul_den : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] {num : ℤ} {den : ℕ} {x : M}, num • 1 ≤ den • x → ∀ {n : ℤ}, x ≤ n • 1 → num ≤ n * ↑den
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `none` if no such key exists.
 -/
Std.TreeMap.getKeyLT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option α
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDivisionCommMonoid : {α : Type u_1} → [DivisionCommMonoid α] → DivisionCommMonoid αᵒᵈ
-- Std.Async.System
Std.Async.System.instInhabitedCPUTimes.default : Std.Async.System.CPUTimes
-- Mathlib.Data.Int.Bitwise
Int.bodd.eq_2 : ∀ (n : ℕ), (Int.negSucc n).bodd = !n.bodd
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.IsSplitEpi f], CategoryTheory.Limits.IsZero Y ↔ f = 0
-- Mathlib.FieldTheory.Finite.Basic
/-- A non-zero `a : F` is a square if and only if `a ^ (#F / 2) = 1`.  -/
FiniteField.isSquare_iff : ∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F],
  ringChar F ≠ 2 → ∀ {a : F}, a ≠ 0 → (IsSquare a ↔ a ^ (Fintype.card F / 2) = 1)
-- Init.Data.SInt.Lemmas
Int32.sub_sub : ∀ (a b c : Int32), a - b - c = a - (b + c)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.coe_vadd : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : VAdd M X]
  [inst_1 : VAdd N Y] [inst_2 : VAdd R Y] [inst_3 : VAddCommClass N R Y] (f : X →ₑ[σ] Y) (r : R), ⇑(r +ᵥ f) = r +ᵥ ⇑f
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.opEpi_id : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (σ : M.GeneratingSections),
  σ.ofEpi (CategoryTheory.CategoryStruct.id M) = σ
-- Mathlib.Topology.ClusterPt
mem_closure_iff_nhds_basis : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort w} {x : X} {t : Set X} {p : ι → Prop} {s : ι → Set X},
  (nhds x).HasBasis p s → (x ∈ closure t ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i)
-- Mathlib.Algebra.GCDMonoid.FinsetLemmas
Finset.Rat.den_prod_dvd_prod_den : ∀ {ι : Type u_3} (s : Finset ι) (f : ι → ℚ), (∏ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den
-- Mathlib.Topology.Algebra.Monoid
instSeparatelyContinuousMulOrderDual : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M], SeparatelyContinuousMul Mᵒᵈ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_log_of_pow_le : ∀ {x y : ℝ} {n : ℕ}, 0 < x → x ^ n ≤ y → ↑n * Real.log x ≤ Real.log y
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.id_comp : ∀ {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {F : Type u_10} {G : Type u_11} [inst : NormedField 𝕜₂] [inst_1 : NormedField 𝕜₃]
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} [inst_2 : AddCommGroup F] [inst_3 : TopologicalSpace F] [inst_4 : Module 𝕜₂ F]
  [inst_5 : AddCommGroup G] [inst_6 : TopologicalSpace G] [inst_7 : Module 𝕜₃ G] (g : F →SWOT[σ₂₃] G),
  g.comp (ContinuousLinearMapWOT.id 𝕜₂ F) = g
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- The composition of `C^n` functions is `C^n`.  -/
ContMDiff.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {n : WithTop ℕ∞} {g : M' → M''},
  ContMDiff I' I'' n g → ContMDiff I I' n f → ContMDiff I I'' n (g ∘ f)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- An abbreviation for `HasLimitsOfShape (Discrete f)`.  -/
CategoryTheory.Limits.HasProductsOfShape : Type v → (C : Type u_1) → [CategoryTheory.Category.{u_2, u_1} C] → Prop
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Real.fourierChar.eq_1 : Real.fourierChar =
  { toFun := fun z => Circle.exp (2 * Real.pi * z), map_zero_eq_one' := Real.fourierChar._proof_1,
    map_add_eq_mul' := ⋯ }
-- Mathlib.Data.Set.Finite.Lattice
Set.infinite_of_not_bddBelow : ∀ {α : Type u} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α] {s : Set α}, ¬BddBelow s → s.Infinite
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.IsAnisotropic.rootForm_root_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : Fintype ι} {inst_1 : AddCommGroup M}
  {inst_2 : AddCommGroup N} {inst_3 : CommRing R} {inst_4 : Module R M} {inst_5 : Module R N} {P : RootPairing ι R M N}
  [self : P.IsAnisotropic] (i : ι), (P.RootForm (P.root i)) (P.root i) ≠ 0
-- Mathlib.Algebra.Tropical.Basic
Tropical.mulRightStrictMono : ∀ {R : Type u} [inst : Preorder R] [inst_1 : Add R] [AddRightStrictMono R], MulRightStrictMono (Tropical R)
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isLocal_adj_unit_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : G ⊣ F) [F.Full] [F.Faithful] (X : D),
  CategoryTheory.ObjectProperty.isLocal (fun x => x ∈ Set.range F.obj) (adj.unit.app X)
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_card_add : ∀ {α : Type u_1} (s : Multiset α) {i : ℕ}, 0 < i → Multiset.powersetCard (s.card + i) s = 0
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.toLimit.eq_1 : ∀ (P : ProfiniteAddGrp.{u}),
  P.toLimit =
    ProfiniteAddGrp.ofHom
      (let __src := P.toLimitFun;
      { toAddMonoidHom := __src, continuous_toFun := ⋯ })
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- The pointwise intersection of an upper hemicontinuous function with a fixed closed set is
upper hemicontinuous.  -/
UpperHemicontinuousAt.inter : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  UpperHemicontinuousAt f x → ∀ {u : Set β}, IsClosed u → UpperHemicontinuousAt (fun x => f x ∩ u) x
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.prod_le_prod_of_subset_of_one_le : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f : ι → R} {s t : Finset ι}, s ⊆ t → (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ t, i ∉ s → 1 ≤ f i) → ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_singleton : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, {a}.inf = a
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.continuousOn_mul : ∀ {A : Type u_7} [inst : NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → A},
  IntervalIntegrable f μ a b → ContinuousOn g (Set.uIcc a b) → IntervalIntegrable (fun x => g x * f x) μ a b
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.State.pendingMVars : Lean.Elab.Term.State → List Lean.MVarId
-- Mathlib.Tactic.Linter.TextBased
/-- A line ends with windows line endings (\r\n) instead of unix ones (\n).  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.windowsLineEnding : Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.Data.PNat.Defs
PNat.coe_le_coe : ∀ (n k : ℕ+), ↑n ≤ ↑k ↔ n ≤ k
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Equivalence.prod_inverse : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D),
  (E₁.prod E₂).inverse = E₁.inverse.prod E₂.inverse
-- Lean.Meta.LazyDiscrTree
/-- Number of elements in result
 -/
Lean.Meta.LazyDiscrTree.MatchResult.size : {α : Type} → Lean.Meta.LazyDiscrTree.MatchResult α → ℕ
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.w_apply' : ∀ {X Y : TopPair} {f g : X ⟶ Y} (H : TopPair.Homotopy f g) (x : ↑TopPair.snd) (t : ↑unitInterval),
  H.fst (t, (CategoryTheory.ConcreteCategory.hom TopPair.map) x) =
    (CategoryTheory.ConcreteCategory.hom TopPair.map) (H.snd (t, x))
-- Mathlib.Data.Matrix.Mul
Matrix.mul_mul_right : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : CommSemiring α] [inst_1 : Fintype n]
  (M : Matrix m n α) (N : Matrix n o α) (a : α), (M * Matrix.of fun i j => a * N i j) = a • (M * N)
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.MatchUnifyResult.args : Lean.Meta.Sym.MatchUnifyResult → Array Lean.Expr
-- Mathlib.Algebra.Order.Group.PosPart
posPart_eq_self : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, a⁺ = a ↔ 0 ≤ a
-- Init.Data.Int.Order
Int.add_le_iff_le_sub : ∀ {a b c : ℤ}, a + b ≤ c ↔ a ≤ c - b
-- Init.Data.SInt.Bitwise
Int32.toBitVec_or : ∀ (a b : Int32), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.self_mem_flag : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)}, i.castSucc < k → b i ∈ b.flag k
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_mul_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.MonObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Multiset.Nat.mem_antidiagonalTuple : ∀ {n k : ℕ} {x : Fin k → ℕ}, x ∈ Multiset.Nat.antidiagonalTuple k n ↔ ∑ i, x i = n
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Compatibility of the monoid and comonoid structures, in terms of morphisms in `C`.  -/
CategoryTheory.Bimon.compatibility_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : C) [inst_3 : CategoryTheory.BimonObj M] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator M M (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
            (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M M).hom M))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
                (CategoryTheory.MonoidalCategoryStruct.associator M M M).hom)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.associator M M
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).inv
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
                  h)))))) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul h)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R),
  ((CategoryTheory.Comma.mapLeftIso R i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredLimit_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], ¬Order.IsPredLimit ⊤
-- Mathlib.Topology.Sequences
IsCompact.tendsto_subseq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FirstCountableTopology X] {s : Set X} {x : ℕ → X},
  IsCompact s → (∀ (n : ℕ), x n ∈ s) → ∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.conjugateEquiv_pullbackId_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (S : CategoryTheory.Sheaf J RingCat),
  (CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.id
        (SheafOfModules.pullbackPushforwardAdjunction (CategoryTheory.CategoryStruct.id S)))
      (SheafOfModules.pullbackId S).hom =
    (SheafOfModules.pushforwardId S).inv
-- Mathlib.RingTheory.QuasiFinite.Weakly
Algebra.QuasiFiniteAt.congr_simp : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p p_1 : Ideal S)
  (e_p : p = p_1) [inst_3 : p.IsPrime], Algebra.QuasiFiniteAt R p = Algebra.QuasiFiniteAt R p_1
-- Init.Data.Nat.Dvd
Nat.pos_of_dvd_of_pos : ∀ {m n : ℕ}, m ∣ n → 0 < n → 0 < m
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.toEquiv_eq_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃ₜ* N), f.toEquiv = ↑f
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange.addEquiv_symm : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → AddZeroClass (β₁ i)]
  [inst_1 : (i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i),
  (DFinsupp.mapRange.addEquiv e).symm = DFinsupp.mapRange.addEquiv fun i => (e i).symm
-- Init.Conv
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any.  -/
Lean.Parser.Tactic.Conv.allGoals : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The canonical surjective group homomorphism `G →* f(G)` induced by a group
homomorphism `G →* N`.  -/
MonoidHom.rangeRestrict : {G : Type u_1} → [inst : Group G] → {N : Type u_5} → [inst_1 : Group N] → (f : G →* N) → G →* ↥f.range
-- Lean.Elab.App
/-- Elaborated arguments.  -/
Lean.Elab.Term.ElabAppArgs.State.fArgs : Lean.Elab.Term.ElabAppArgs.State → Array Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.edge_mk : ∀ {V : Type u_1} {G : SimpleGraph V} {p : V × V} (h : G.Adj p.1 p.2), { toProd := p, adj := h }.edge = s(p.1, p.2)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.isExtremal_top_free_iff_isTuranMaximal : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {α : Type u_2}
  [inst_2 : Fintype α] [Nontrivial α], G.IsExtremal ⊤.Free ↔ G.IsTuranMaximal (Fintype.card α - 1)
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.normOneClass : ∀ {α : Type u_2} [inst : SeminormedAddCommGroup α] [inst_1 : One α] [NormOneClass α], NormOneClass (ULift.{u_5, u_2} α)
-- Batteries.Lean.Meta.Basic
/-- Run a computation with hygiene turned off.
 -/
Lean.Meta.unhygienic : {m : Type → Type} → {α : Type} → [Lean.MonadWithOptions m] → m α → m α
-- Mathlib.Analysis.Calculus.Deriv.Inv
derivWithin_fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x →
    DifferentiableWithinAt 𝕜 d s x →
      d x ≠ 0 → derivWithin (fun x => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.mkENodeCore.unsafe_1 : (e : Lean.Expr) →
  (n : Lean.Meta.Grind.ENode) →
    (s : Lean.Meta.Grind.Goal) → Lean.Meta.Grind.CongrTable (Lean.PersistentHashMap.insert s.enodeMap { expr := e } n)
-- Init.Data.Order.Lemmas
Std.le_of_lt : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] {a b : α}, a < b → a ≤ b
-- Init.Data.List.Lex
List.lex_irrefl : ∀ {α : Type u_1} {r : α → α → Prop}, (∀ (x : α), ¬r x x) → ∀ (l : List α), ¬List.Lex r l l
-- Init.Data.UInt.Bitwise
UInt16.and_comm : ∀ (a b : UInt16), a &&& b = b &&& a
-- Mathlib.Algebra.FiveLemma
/-- A special case of the five lemma in terms of modules. For a diagram explaining the variables,
see the module docstring.  -/
LinearMap.bijective_of_bijective_of_injective_of_left_exact : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_7} {N₂ : Type u_8}
  {N₃ : Type u_9} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃]
  [inst_4 : Module R M₁] [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁]
  [inst_8 : AddCommGroup N₂] [inst_9 : AddCommGroup N₃] [inst_10 : Module R N₁] [inst_11 : Module R N₂]
  [inst_12 : Module R N₃] (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (i₁ : M₁ →ₗ[R] N₁)
  (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃),
  g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁ →
    g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Bijective ⇑i₂ →
            Function.Injective ⇑i₃ → Function.Injective ⇑f₁ → Function.Injective ⇑g₁ → Function.Bijective ⇑i₁
-- Mathlib.Topology.Homotopy.HSpaces
IsTopologicalAddGroup.toHSpace.eq_1 : ∀ (M : Type u) [inst : AddZeroClass M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousAdd M],
  IsTopologicalAddGroup.toHSpace M =
    { hmul := { toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }, e := 0, hmul_e_e := ⋯,
      eHmul :=
        (ContinuousMap.HomotopyRel.refl
              ({ toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }.comp
                ((ContinuousMap.const M 0).prodMk (ContinuousMap.id M)))
              {0}).cast
          ⋯ ⋯,
      hmulE :=
        (ContinuousMap.HomotopyRel.refl
              ({ toFun := Function.uncurry Add.add, continuous_toFun := ⋯ }.comp
                ((ContinuousMap.id M).prodMk (ContinuousMap.const M 0)))
              {0}).cast
          ⋯ ⋯ }
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Coinduction principle for proving `Sorted`. Given a predicate `motive` on multiseries,
if `motive ms` holds (base case) and the predicate "survives" destruction of its argument, then
`ms` is `Sorted`. Here "survives" means that if `x = cons (exp, coef) tl`, then `motive x` must
imply `coef.Sorted`, `tl.leadingExp < exp`, and `motive tl`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.coind : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  (motive : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl → Prop),
  motive s →
    (∀ (exp : ℝ) (coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)
        (tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
        motive (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) →
          coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl) →
      s.Sorted
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
left_le_lineMap_iff_nonneg : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r : k}, a < b → (a ≤ (AffineMap.lineMap a b) r ↔ 0 ≤ r)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_eq_toArray_map : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  Std.DTreeMap.Internal.Impl.Const.toArray t = (List.map (fun e => (e.fst, e.snd)) t.toListModel).toArray
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂)
  (i : m) (j : n), (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
-- Mathlib.Algebra.Group.Equiv.Defs
MonoidHomClass.toMonoidHom.congr_simp : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [inst_3 : MonoidHomClass F M N] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Analysis.LocallyConvex.Basic
/-- **Alias** of the forward direction of `balanced_iff_smul_mem`. -/
Balanced.smul_mem : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E},
  Balanced 𝕜 s → ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s