mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Tape
/-- We can cons an element onto a `ListBlank`.  -/
Turing.ListBlank.cons : {Γ : Type u_1} → [inst : Inhabited Γ] → Γ → Turing.ListBlank Γ → Turing.ListBlank Γ
-- Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
/-- Let `b` be a basis for `M` over `ℤ` and `bN` a basis for `N` over `ℤ` of the same dimension.
Then an alternative way to compute the cardinality of `M ⧸ N` is given by taking the determinant
of `bN` over `b`.  -/
Submodule.natAbs_det_basis_change : ∀ {M : Type u_1} [inst : AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] {ι : Type u_2} [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι] (b : Module.Basis ι ℤ M) (N : Submodule ℤ M) (bN : Module.Basis ι ℤ ↥N),
  (b.det (Subtype.val ∘ ⇑bN)).natAbs = Nat.card (M ⧸ N)
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.trans : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [Algebra.IsStandardOpenImmersion R S] [Algebra.IsStandardOpenImmersion S T], Algebra.IsStandardOpenImmersion R T
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Coindep.coindep_contract_of_disjoint : ∀ {α : Type u_1} {M : Matroid α} {X C : Set α}, M.Coindep X → Disjoint X C → (M.contract C).Coindep X
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piCurry_symm_apply : ∀ {ι : Type u_6} {κ : ι → Type u_7} (X : (i : ι) → κ i → Type u_8)
  [inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)] (f : (x : ι) → (y : κ x) → X x y) (x : Sigma κ),
  (MeasurableEquiv.piCurry X).symm f x = Sigma.uncurry f x
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.eLpNormLESNormFDerivOfLeConst_def : ∀ (F : Type u_6) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_7} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure] [inst_8 : FiniteDimensional ℝ F] (s : Set E)
  (p q : NNReal),
  MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ s p q =
    have p' := (p⁻¹ - (↑(Module.finrank ℝ E))⁻¹)⁻¹;
    (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p') * MeasureTheory.SNormLESNormFDerivOfEqConst F μ ↑p
-- Mathlib.Data.Finset.Sups
Finset.infs_sups_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] (s t u : Finset α), s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mem_coe : ∀ {P : Type u_2} [inst : MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P},
  p ∈ Metric.sphere s.center s.radius ↔ p ∈ s
-- Lean.Meta.Basic
Lean.Meta.ParamInfo.isExplicit : Lean.Meta.ParamInfo → Bool
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A],
  IsIntegrallyClosedIn (↥(integralClosure R A).toSubring) A
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- For a manifold `M` and a smooth homomorphism `φ` between abelian additive Lie
groups `A`, `A'`, the 'left-composition-by-`φ`' morphism of sheaves from
`smoothSheafAddCommGroup IM I M A` to `smoothSheafAddCommGroup IM I' M A'`.  -/
smoothSheafAddCommGroup.compLeft : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            {H' : Type u_6} →
                              [inst_7 : TopologicalSpace H'] →
                                (I' : ModelWithCorners 𝕜 E H') →
                                  (M : Type u) →
                                    [inst_8 : TopologicalSpace M] →
                                      [inst_9 : ChartedSpace HM M] →
                                        (A A' : Type u) →
                                          [inst_10 : TopologicalSpace A] →
                                            [inst_11 : ChartedSpace H A] →
                                              [inst_12 : TopologicalSpace A'] →
                                                [inst_13 : ChartedSpace H' A'] →
                                                  [inst_14 : AddCommGroup A] →
                                                    [inst_15 : AddCommGroup A'] →
                                                      [inst_16 : LieAddGroup I (↑⊤) A] →
                                                        [inst_17 : LieAddGroup I' (↑⊤) A'] →
                                                          (φ : A →+ A') →
                                                            ContMDiff I I' ↑⊤ ⇑φ →
                                                              (smoothSheafAddCommGroup IM I M A ⟶
                                                                smoothSheafAddCommGroup IM I' M A')
-- Mathlib.Data.Set.Card
Set.encard_insert_of_notMem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → (insert a s).encard = s.encard + 1
-- Mathlib.Algebra.GroupWithZero.Basic
ne_zero_of_one_div_ne_zero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, 1 / a ≠ 0 → a ≠ 0
-- Mathlib.Order.Lattice
Prod.sup_def : ∀ (α : Type u) (β : Type v) [inst : Max α] [inst_1 : Max β] (p q : α × β), p ⊔ q = (p.1 ⊔ q.1, p.2 ⊔ q.2)
-- Mathlib.RingTheory.Polynomial.Content
/-- The primitive part of a polynomial `p` is the primitive polynomial gained by dividing `p` by
`p.content`. If `p = 0`, then `p.primPart = 1`.  -/
Polynomial.primPart : {R : Type u_1} → [inst : CommRing R] → [NormalizedGCDMonoid R] → Polynomial R → Polynomial R
-- Mathlib.Data.Set.Function
Set.BijOn.compl : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.BijOn f s t → Function.Bijective f → Set.BijOn f sᶜ tᶜ
-- Mathlib.Algebra.Group.Opposite
MulOpposite.op_zpow : ∀ {α : Type u_1} [inst : DivInvMonoid α] (x : α) (z : ℤ), MulOpposite.op (x ^ z) = MulOpposite.op x ^ z
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_null : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  DividedPowerAlgebra.dp R n 0 = if n = 0 then 1 else 0
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- **Alias** of the forward direction of `Matrix.isElliptic_neg_iff`. -/
Matrix.IsElliptic.of_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R},
  (-m).IsElliptic → m.IsElliptic
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.map.congr_simp : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn fn_1 : N₁ →* N₂)
  (e_fn : fn = fn_1) (fg fg_1 : G₁ →* G₂) (e_fg : fg = fg_1)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn),
  SemidirectProduct.map fn fg h = SemidirectProduct.map fn_1 fg_1 ⋯
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableAdd : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Add (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableAdd (α i)], MeasurableAdd ((i : ι) → α i)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_sup : ∀ {M : Type u_2} [inst : AddZeroClass M] (S₁ S₂ : AddSubmonoid Mᵃᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.e_isoExt_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
  (hF' : CategoryTheory.Limits.IsImage F'), CategoryTheory.CategoryStruct.comp F'.e (hF.isoExt hF').inv = F.e
-- Mathlib.Computability.Language
/-- `Language.reverse` as a ring isomorphism to the opposite ring.  -/
Language.reverseIso : (α : Type u_1) → Language α ≃+* (Language α)ᵐᵒᵖ
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_univ_eq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ Set.univ = 0 ↔ μ = 0
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : σ) (p : MvPolynomial σ R),
  MvPolynomial.degreeOf n p = Multiset.count n p.degrees
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.id_comp : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁ →qᵢ Q₂),
  (QuadraticMap.Isometry.id Q₂).comp f = f
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- Every basis vector from `adjustToOrientation` is either that from the original basis or its
negation.  -/
OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι) [inst_4 : Nonempty ι] (i : ι),
  (e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (Std.Internal.List.insertEntry k v l) = (k == a || Std.Internal.List.containsKey a l)
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.zsmul_eq_intCast_mul : ∀ {α : Type u} [inst : Lean.Grind.Ring α] {k : ℤ} {a : α}, k • a = ↑k * a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 = 0 → IsUnit (P 0)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_eq_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A} {x : NNReal}, 0 < x → a ^ x = a ^ ↑x
-- Mathlib.Algebra.Free
FreeSemigroup.of_head : ∀ {α : Type u} (x : α), (FreeSemigroup.of x).head = x
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheckSite.moduleDoc.sizeOf_spec : ∀ (n : ℕ), sizeOf (Lean.Doc.DeferredCheckSite.moduleDoc n) = 1 + sizeOf n
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.smul_closure : ∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (a : M)
  (s : Set R), a • Ideal.span s = Ideal.span (a • s)
-- Mathlib.AlgebraicGeometry.Sites.Etale
AlgebraicGeometry.Scheme.zariskiTopology_le_etaleTopology : AlgebraicGeometry.Scheme.zariskiTopology ≤ AlgebraicGeometry.Scheme.etaleTopology
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.mk : {X : Type u_1} →
  {G : Type u_2} →
    [inst : SMul G X] →
      (toPartialEquiv : PartialEquiv X X) →
        (∃ S, Equidecomp.IsDecompOn (↑toPartialEquiv) toPartialEquiv.source S) → Equidecomp X G
-- Mathlib.Combinatorics.Young.SemistandardTableau
/-- The "highest weight" SSYT of a given shape has all i's in row i, for each i.  -/
SemistandardYoungTableau.highestWeight : (μ : YoungDiagram) → SemistandardYoungTableau μ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitArg.app : Lean.Meta.Grind.SplitArg → Lean.Expr
-- Mathlib.Analysis.Calculus.LagrangeMultipliers
/-- Lagrange multipliers theorem: if `φ : E → ℝ` has a local extremum on the set `{x | f x = f x₀}`
at `x₀`, and both `f : E → ℝ` and `φ` are strictly differentiable at `x₀`, then there exist
`a b : ℝ` such that `(a, b) ≠ 0` and `a • f' + b • φ' = 0`.  -/
IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {φ : E → ℝ} {x₀ : E}
  {φ' : StrongDual ℝ E} {f : E → ℝ} {f' : StrongDual ℝ E},
  IsLocalExtrOn φ {x | f x = f x₀} x₀ →
    HasStrictFDerivAt f f' x₀ → HasStrictFDerivAt φ φ' x₀ → ∃ a b, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
-- Mathlib.Algebra.Ring.Action.Group
MulSemiringAction.toRingEquiv_apply_apply : ∀ (G : Type u_1) [inst : Group G] (R : Type u_2) [inst_1 : Semiring R] [inst_2 : MulSemiringAction G R] (x : G) (a : R),
  ((MulSemiringAction.toRingEquiv G R) x) a = x • a
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_insertIdx : ∀ {M : Type u_4} [inst : AddMonoid M] {l : List M} {a : M} {i : ℕ},
  i ≤ l.length → (∀ a' ∈ List.take i l, AddCommute a a') → (l.insertIdx i a).sum = a + l.sum
-- Mathlib.Data.List.Cycle
List.next_mem : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ l), l.next x h ∈ l
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.IsIntegral.eq_bot_of_comap_eq_bot : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] [IsDomain A] [Nontrivial R] {I : Ideal A}, Ideal.comap (algebraMap R A) I = ⊥ → I = ⊥
-- Mathlib.Data.Part
/-- Convert a `Part α` with a decidable domain to an option  -/
Part.toOption : {α : Type u_1} → (o : Part α) → [Decidable o.Dom] → Option α
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_congr : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
  f =ᵐ[μ] g → μ.tilted f = μ.tilted g
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mk.inj : ∀ {K : Type u_1} {L : Type u_2} {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L}
  {toSubalgebra : Subalgebra K L} {inv_mem' : ∀ x ∈ toSubalgebra.carrier, x⁻¹ ∈ toSubalgebra.carrier}
  {toSubalgebra_1 : Subalgebra K L} {inv_mem'_1 : ∀ x ∈ toSubalgebra_1.carrier, x⁻¹ ∈ toSubalgebra_1.carrier},
  { toSubalgebra := toSubalgebra, inv_mem' := inv_mem' } = { toSubalgebra := toSubalgebra_1, inv_mem' := inv_mem'_1 } →
    toSubalgebra = toSubalgebra_1
-- Mathlib.RingTheory.Valuation.RankOne
/-- If `v` is a rank one valuation and `x : Γ₀` has image `0` under `RankOne.hom v`, then
`x = 0`.  -/
Valuation.RankOne.zero_of_hom_zero : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  [hv : v.RankOne] {x : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, (Valuation.RankOne.hom v) x = 0 → x = 0
-- Mathlib.GroupTheory.Index
/-- **Alias** of `Subgroup.isFiniteRelIndex_of_le_left`. -/
Subgroup.isFiniteRelIndex_of_le : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (L : Subgroup G) [H.IsFiniteRelIndex L],
  H ≤ K → K.IsFiniteRelIndex L
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Millisecond.Ordinal n
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.mk.sizeOf_spec : ∀ {M : Type u_10} {N : Type u_11} [inst : One M] [inst_1 : One N] [inst_2 : SizeOf M] [inst_3 : SizeOf N]
  (toFun : M → N) (map_one' : toFun 1 = 1), sizeOf { toFun := toFun, map_one' := map_one' } = 1 + sizeOf map_one'
-- Mathlib.Tactic.Ring.Common
/-- A product `x ^ e * b` is a monomial if `b` is a monomial. Here `x` is an `ExBaseNat`
and `e` is an `ExProdNat` representing a monomial expression in `ℕ` (it is a monomial instead of
a polynomial because we eagerly normalize `x ^ (a + b) = x ^ a * x ^ b`.)  -/
Mathlib.Tactic.Ring.Common.ExProdNat.mul : {x e b : Q(ℕ)} →
  Mathlib.Tactic.Ring.Common.ExBaseNat x →
    Mathlib.Tactic.Ring.Common.ExProdNat e →
      Mathlib.Tactic.Ring.Common.ExProdNat b → Mathlib.Tactic.Ring.Common.ExProdNat q(«$x» ^ «$e» * «$b»)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.forget₂_obj : ∀ {R : Type u} [inst : CommRing R] (X : QuadraticModuleCat R),
  (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X.toModuleCat
-- Mathlib.Order.CountableDenseLinearOrder
/-- For each `a`, we can find a `b` in the codomain, such that `a`'s relation to
the domain of `f` is `b`'s relation to the image of `f`.

Thus, if `a` is not already in `f`, then we can extend `f` by sending `a` to `b`.
 -/
Order.PartialIso.exists_across : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [DenselyOrdered β] [NoMinOrder β]
  [NoMaxOrder β] [Nonempty β] (f : Order.PartialIso α β) (a : α), ∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
-- Mathlib.Order.InitialSeg
PrincipalSeg.map_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : PartialOrder α] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] (f : α <i β), f.toRelEmbedding ⊥ = ⊥
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH1_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.shortComplexH1 A).f = groupHomology.d₂₁ A
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_iff_eq_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsPath ↔ p = SimpleGraph.Walk.nil
-- Mathlib.Algebra.Group.Action.Opposite
AddSemigroup.opposite_vaddCommClass' : ∀ {α : Type u_3} [inst : AddSemigroup α], VAddCommClass α αᵃᵒᵖ α
-- Mathlib.RingTheory.Localization.Away.Lemmas
IsLocalization.Away.span_range_mulNumerator_eq_top : ∀ {R : Type u_1} [inst : CommRing R] {s : Set R},
  Ideal.span s = ⊤ →
    ∀ {Rₜ : ↑s → Type u_2} [inst_1 : (t : ↑s) → CommRing (Rₜ t)] [inst_2 : (t : ↑s) → Algebra R (Rₜ t)]
      [inst_3 : ∀ (t : ↑s), IsLocalization.Away (↑t) (Rₜ t)] {p : (t : ↑s) → Set (Rₜ t)},
      (∀ (r : ↑s), Ideal.span (p r) = ⊤) → Ideal.span (Set.range (IsLocalization.Away.mulNumerator s p)) = ⊤
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Given an `R`-module M, consider Hom(S, M) -- the `R`-linear maps between S (as an `R`-module by
means of restriction of scalars) and M. `S` acts on Hom(S, M) by `s • g = x ↦ g (x • s)`
 -/
ModuleCat.CoextendScalars.hasSMul : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (M : Type v) →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] → SMul S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] M)
-- Mathlib.RingTheory.Jacobson.Radical
Module.comap_jacobson_of_ker_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Surjective ⇑f → f.ker ≤ Module.jacobson R M → Submodule.comap f (Module.jacobson R₂ M₂) = Module.jacobson R M
-- Mathlib.RepresentationTheory.FDRep
FDRep.instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ : {R : Type u} →
  {G : Type v} → [inst : CommRing R] → [inst_1 : Monoid G] → CategoryTheory.HasForget₂ (FDRep R G) (Rep.{u, u, v} R G)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.retract_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left h.i) (CategoryTheory.Arrow.Hom.left h.r) =
    CategoryTheory.CategoryStruct.id X
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Core function that delaborates a rational literal that is the division of an integer literal
by a natural number literal.
The division must be homogeneous for it to count as a rational literal.
 -/
Lean.PrettyPrinter.Delaborator.delabDivRatCore : optParam Bool false → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_surjective_iff_closure_range_eq_top : ∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β},
  Function.Surjective ⇑(FreeGroup.lift f) ↔ Subgroup.closure (Set.range f) = ⊤
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.filterMap.go.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → Option (γ a))
  (acc : Std.DHashMap.Internal.AssocList α γ),
  Std.DHashMap.Internal.AssocList.filterMap.go✝ f acc Std.DHashMap.Internal.AssocList.nil = acc
-- Mathlib.NumberTheory.NumberField.EquivReindex
NumberField.conj_basisMatrix : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.basisMatrix K).map ⇑(starRingEnd ℂ) =
    (Matrix.reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm NumberField.ComplexEmbedding.conjugate ⋯))
      (NumberField.basisMatrix K)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_div : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (m : F),
  Function.Injective ⇑m → ∀ {s t : Set β}, s ⊆ Set.range ⇑m → t ⊆ Set.range ⇑m → ⇑m ⁻¹' (s / t) = ⇑m ⁻¹' s / ⇑m ⁻¹' t
-- Mathlib.Topology.Homotopy.Equiv
/-- A homotopy equivalence between topological spaces `X` and `Y` are a pair of functions
`toFun : C(X, Y)` and `invFun : C(Y, X)` such that `toFun.comp invFun` and `invFun.comp toFun`
are both homotopic to corresponding identity maps.
 -/
ContinuousMap.«term_≃ₕ_» : Lean.TrailingParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α},
  (a == b) = true → Std.Internal.List.containsKey a l = Std.Internal.List.containsKey b l
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] [inst_2 : DecidableEq α] (a : α) (x : M),
  MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq a x =
    MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq._aux_1 a x
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.subgroupOf_inertia : ∀ {M : Type u_6} [inst : AddGroup M] (I : AddSubgroup M) {G : Type u_7} [inst_1 : Group G] [inst_2 : MulAction G M]
  (H : Subgroup G), (I.inertia G).subgroupOf H = I.inertia ↥H
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_comp_lift_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {Q : Type u_4} [inst_2 : AddCommMonoid Q] (k : S.LocalizationMap Q) {A : Type u_5}
  [inst_3 : AddCommMonoid A] {l : M →+ A} (hl : ∀ (w : ↥S), IsAddUnit (l ↑w)), (k.lift hl).comp (f.lift ⋯) = f.lift hl
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.algebraMap_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : CommSemiring S] [inst_5 : Module S M]
  [inst_6 : SMulCommClass R S M] [inst_7 : SMul S R] [inst_8 : IsScalarTower S R M] [inst_9 : ContinuousConstSMul S M]
  [inst_10 : IsTopologicalAddGroup M] (r : S) (m : M), ((algebraMap S (M →L[R] M)) r) m = r • m
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atTop_atTop_of_monotone : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → (∀ (b : β), ∃ a, b ≤ f a) → Filter.Tendsto f Filter.atTop Filter.atTop