mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Interval
/-- The embedding into an interval from a sub-interval lying on the left, as a `ContinuousMap`.  -/
ContinuousMap.IccInclusionLeft : {α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] → {a b c : α} → [Fact (b ≤ c)] → C(↑(Set.Icc a b), ↑(Set.Icc a c))
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₂_D₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂' i₁₂'') h) =
    CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂' i₁₂'')) h
-- Lean.Meta.Basic
/-- Returns the inferred type of the given expression. Assumes the expression is type-correct.

The type inference algorithm does not do general type checking.
Type inference only looks at subterms that are necessary for determining an expression's type,
and as such if `inferType` succeeds it does *not* mean the term is type-correct.
If an expression is sufficiently ill-formed that it prevents `inferType` from computing a type,
then it will fail with a type error.

For typechecking during elaboration, see `Lean.Meta.check`.
(Note that we do not guarantee that the elaborator typechecker is as correct or as efficient as
the kernel typechecker. The kernel typechecker is invoked when a definition is added to the environment.)

Here are examples of type-incorrect terms for which `inferType` succeeds:
```lean
public import Lean

public section

open Lean Meta

/--
`@id.{1} Bool Nat.zero`.
In general, the type of `@id α x` is `α`.
-/
def e1 : Expr := mkApp2 (.const ``id [1]) (.const ``Bool []) (.const ``Nat.zero [])
#eval inferType e1
-- Lean.Expr.const `Bool []
#eval check e1
-- error: application type mismatch

/--
`let x : Int := Nat.zero; true`.
In general, the type of `let x := v; e`, if `e` does not reference `x`, is the type of `e`.
-/
def e2 : Expr := .letE `x (.const ``Int []) (.const ``Nat.zero []) (.const ``true []) false
#eval inferType e2
-- Lean.Expr.const `Bool []
#eval check e2
-- error: invalid let declaration
```
Here is an example of a type-incorrect term that makes `inferType` fail:
```lean
/--
`Nat.zero Nat.zero`
-/
def e3 : Expr := .app (.const ``Nat.zero []) (.const ``Nat.zero [])
#eval inferType e3
-- error: function expected
```

See `Lean.Meta.inferTypeImp` for the implementation of `inferType`.
 -/
Lean.Meta.inferType : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- If the measurable set `A` is norm-stable at complex places in the sense that
`normAtComplexPlaces⁻¹ (normAtComplexPlaces '' A) = A`, then its volume can be computed via an
integral over `normAtComplexPlaces '' A`.
 -/
NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral : ∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)} [inst_1 : NumberField K],
  NumberField.mixedEmbedding.normAtComplexPlaces ⁻¹' NumberField.mixedEmbedding.normAtComplexPlaces '' A = A →
    MeasurableSet A →
      MeasureTheory.volume A =
        ENNReal.ofReal (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in NumberField.mixedEmbedding.normAtComplexPlaces '' A,
            ∏ w, ENNReal.ofReal (x ↑w)
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.of_pushout_inr_of_descendsAlong : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {Z X Y : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} [P.CodescendsAlong Q] [inst_2 : CategoryTheory.Limits.HasPushout f g],
  Q g → P (CategoryTheory.Limits.pushout.inr f g) → P f
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.col_submatrix_eq_comp : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {m₀ : Type u_10} {n₀ : Type u_11} (A : Matrix m n α) (r : m₀ → m)
  (c : n₀ → n) (j : n₀), (A.submatrix r c).col j = A.col (c j) ∘ r
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.Channel.mk.inj : ∀ {α : Type} {inner inner_1 : Std.CloseableChannel α}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instFaithfulModuleCatFunctor : ∀ (R : Type u) [inst : Ring R], (LightCondMod.LocallyConstant.functor R).Faithful
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumberNat_zero : ruzsaSzemerediNumberNat 0 = 0
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIsoX.eq_1 : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j : J),
  K.totalFlipIsoX c j =
    { hom := K.flip.totalDesc fun i₂ i₁ h => c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯,
      inv := K.totalDesc fun i₁ i₂ h => c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.mem_lipschitzGroup : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q},
  x ∈ pinGroup Q → x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.even_card_aut_of_not_isUnramified : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  ¬NumberField.InfinitePlace.IsUnramified k w → Even (Nat.card Gal(K/k))
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- **Alias** of `MeromorphicOn.circleIntegrable_posLog_norm`.

---

If `f` is complex meromorphic on a circle in the complex plane, then `log⁺ ‖f ·‖` is circle
integrable over that circle.
 -/
circleIntegrable_posLog_norm_meromorphicOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.sphere c |R|) → CircleIntegrable (fun x => ‖f x‖.posLog) c R
-- Mathlib.FieldTheory.IsPerfectClosure
IsPRadical.ker_le' : ∀ {K : Type u_1} {L : Type u_2} {inst : CommSemiring K} {inst_1 : CommSemiring L} {i : K →+* L} {p : ℕ}
  [self : IsPRadical i p], RingHom.ker i ≤ pNilradical K p
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
_private.Lean.Meta.Tactic.Simp.Arith.Nat.Basic.0.Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearExpr.visit : Lean.Expr → Lean.Meta.Simp.Arith.Nat.ToLinear.M Lean.Meta.Simp.Arith.Nat.LinearExpr
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- **Alias** of the reverse direction of `toZ_le_toZ`. -/
toZ_mono : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i j : ι}, i ≤ j → toZ i0 i ≤ toZ i0 j
-- Init.Data.String.Iter.Intercalate
/-- Appends the elements of the iterator into a string, placing the separator `s` between them.
 -/
Std.Iter.intercalateString : {α β : Type} → [Std.Iterator α Id β] → [ToString β] → String.Slice → Std.Iter β → String
-- Init.Data.Array.Attach
Array.getElem_attachWith : ∀ {α : Type u_1} {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a} {i : ℕ} (h : i < (xs.attachWith P H).size),
  (xs.attachWith P H)[i] = ⟨xs[i], ⋯⟩
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A kernel fork for the kernel of `biprod.fst`. It consists of the
morphism `biprod.inr`.  -/
CategoryTheory.Limits.biprod.fstKernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.KernelFork CategoryTheory.Limits.biprod.fst
-- Init.Data.UInt.Lemmas
UInt8.toFin_toBitVec : ∀ (x : UInt8), x.toBitVec.toFin = x.toFin
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k},
  (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback
-- Mathlib.Algebra.Ring.CentroidHom
/-- Commutativity of centroid homomorphisms with right multiplication.  -/
CentroidHomClass.map_mul_right : ∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : NonUnitalNonAssocSemiring α} {inst_1 : FunLike F α α}
  [self : CentroidHomClass F α] (f : F) (a b : α), f (a * b) = f a * b
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Given a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` and a map `p : I₁ × I₂ × I₃ → J`,
this is the functor
`GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject J C₄`
sending `X₁ : GradedObject I₁ C₁`, `X₂ : GradedObject I₂ C₂` and `X₃ : GradedObject I₃ C₃`
to the `J`-graded object sending `j` to the coproduct of
`((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃)` for `p ⟨i₁, i₂, i₃⟩ = j`.  -/
CategoryTheory.GradedObject.mapTrifunctorMap : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) →
                  {I₁ : Type u_7} →
                    {I₂ : Type u_8} →
                      {I₃ : Type u_9} →
                        {J : Type u_10} →
                          (p : I₁ × I₂ × I₃ → J) →
                            [∀ (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
                                  (X₃ : CategoryTheory.GradedObject I₃ C₃),
                                  ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj
                                        X₃).HasMap
                                    p] →
                              CategoryTheory.Functor (CategoryTheory.GradedObject I₁ C₁)
                                (CategoryTheory.Functor (CategoryTheory.GradedObject I₂ C₂)
                                  (CategoryTheory.Functor (CategoryTheory.GradedObject I₃ C₃)
                                    (CategoryTheory.GradedObject J C₄)))
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- Given a monotone family `U` of complete submodules of `E` and a fixed `x : E`,
the orthogonal projection of `x` on `U i` tends to the orthogonal projection of `x` on
`(⨆ i, U i).topologicalClosure` along `atTop`.  -/
Submodule.starProjection_tendsto_closure_iSup : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Preorder ι] (U : ι → Submodule 𝕜 E) [inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection]
  [inst_5 : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection],
  Monotone U →
    ∀ (x : E),
      Filter.Tendsto (fun i => (U i).starProjection x) Filter.atTop
        (nhds ((⨆ i, U i).topologicalClosure.starProjection x))
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.Lean.Json
Lean.instFromJsonPUnit_mathlib.fromJson : Lean.Json → Except String PUnit.{u_1 + 1}
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- Constructor for `IsTriangulated C` which shows that it suffices to obtain an octahedron
for a suitable isomorphic diagram instead of the given diagram.  -/
CategoryTheory.IsTriangulated.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  (∀ ⦃X₁' X₂' X₃' : C⦄ (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃'),
      ∃ X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ u₁₂ u₂₃ e₁ e₂ e₃,
        ∃ (_ : CategoryTheory.CategoryStruct.comp u₁₂' e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom u₁₂) (_ :
          CategoryTheory.CategoryStruct.comp u₂₃' e₃.hom = CategoryTheory.CategoryStruct.comp e₂.hom u₂₃),
          ∃ v₁₂ w₁₂,
            ∃ (h₁₂ :
              CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                CategoryTheory.Pretriangulated.distinguishedTriangles),
              ∃ v₂₃ w₂₃,
                ∃ (h₂₃ :
                  CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                    CategoryTheory.Pretriangulated.distinguishedTriangles),
                  ∃ v₁₃ w₁₃,
                    ∃ (h₁₃ :
                      CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.comp u₁₂ u₂₃) v₁₃ w₁₃ ∈
                        CategoryTheory.Pretriangulated.distinguishedTriangles),
                      Nonempty (CategoryTheory.Triangulated.Octahedron ⋯ h₁₂ h₂₃ h₁₃)) →
    CategoryTheory.IsTriangulated C
-- Lean.Language.Basic
Lean.Language.SnapshotTask.ReportingRange.some.inj : ∀ {range range_1 : Lean.Syntax.Range},
  Lean.Language.SnapshotTask.ReportingRange.some range = Lean.Language.SnapshotTask.ReportingRange.some range_1 →
    range = range_1
-- Mathlib.GroupTheory.OrderOfElement
Function.Injective.isOfFinOrder_iff : ∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] {x : G} [inst_1 : Monoid H] {f : G →* H},
  Function.Injective ⇑f → (IsOfFinOrder (f x) ↔ IsOfFinOrder x)
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_X : ∀ {K : Type u} [inst : Field K], RatFunc.X.intDegree = 1
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.ind : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] {β : AddOreLocalization S X → Prop},
  (∀ (r : X) (s : ↥S), β (r -ₒ s)) → ∀ (q : AddOreLocalization S X), β q
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.instFiniteArrowDiscrete : ∀ (X : Type u) [Finite X], Finite (CategoryTheory.Arrow (CategoryTheory.Discrete X))
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.natPow_one : ∀ {a : ℕ}, a.pow 1 = a
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.directSum_decompose_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] [_hT : Fact T.IsSymmetric] (x : E) (μ : Module.End.Eigenvalues T),
  ((DirectSum.decompose fun μ => Module.End.eigenspace T (↑T 1 μ)) x) μ =
    (Module.End.eigenspace T (↑T 1 μ)).orthogonalProjectionOnto x
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instInhabitedRange.default : Lean.Lsp.Range
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackIso_hom_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : CategoryTheory.PreZeroHypercover T)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f]
  (a : (CategoryTheory.PreZeroHypercover.pullback₁ f E).I₀),
  (CategoryTheory.PreZeroHypercover.pullbackIso f E).hom.s₀ a = id a
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the forward direction of `SimpleGraph.isIndContained_iff_exists_iso_subgraph`. -/
SimpleGraph.IsIndContained.exists_iso_subgraph : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, G.IsIndContained H → ∃ H' _e, H'.IsInduced
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- For `1 ≤ r`, the characteristic function for the zeros of `f * g` is less than or equal to the sum
of the characteristic functions for the zeros of `f` and `g`, respectively.
 -/
ValueDistribution.characteristic_mul_zero_le : ∀ {f₁ f₂ : ℂ → ℂ} {r : ℝ},
  1 ≤ r →
    Meromorphic f₁ →
      (∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) →
        Meromorphic f₂ →
          (∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) →
            ValueDistribution.characteristic (f₁ * f₂) 0 r ≤
              (ValueDistribution.characteristic f₁ 0 + ValueDistribution.characteristic f₂ 0) r
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- If `A`, `B` and `C` have the module topology, and if furthermore `A` is a finite `R`-module,
then any bilinear map `A × B → C` is automatically continuous
 -/
IsModuleTopology.continuous_bilinear_of_finite_left : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [IsTopologicalRing R] {A : Type u_2}
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3}
  [inst_6 : AddCommGroup B] [inst_7 : Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B] {C : Type u_4}
  [inst_9 : AddCommGroup C] [inst_10 : Module R C] [aC : TopologicalSpace C] [IsModuleTopology R C] [Module.Finite R A]
  (bil : A →ₗ[R] B →ₗ[R] C), Continuous fun ab => (bil ab.1) ab.2
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_swap_mul_ge_support_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) (x y : α),
  f.support \ {x, y} ⊆ (Equiv.swap x y * f).support
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- The degree of `K` times the regulator of the family `u` is equal to the absolute value of the
determinant of the matrix whose columns are
`(mult w * log w (fundSystem K i))_i, w` and the column `(mult w)_w`.
 -/
NumberField.Units.finrank_mul_regOfFamily_eq_det : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) (w' : NumberField.InfinitePlace K)
  (e : { w // w ≠ w' } ≃ Fin (NumberField.Units.rank K)),
  ↑(Module.finrank ℚ K) * NumberField.Units.regOfFamily u =
    |(Matrix.of fun i w =>
          if h : i = w' then ↑w.mult
          else ↑w.mult * Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u (e ⟨i, h⟩))))).det|
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.topEquiv_toMonoidHom : ∀ {M : Type u_5} [inst : MulOneClass M], ↑Submonoid.topEquiv = ⊤.subtype
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.precylinder_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] (K : HomologicalComplex C c)
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  K.precylinder.π = HomologicalComplex.cylinder.π K
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.coe_toAdditive_range : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G'),
  (MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range
-- Mathlib.Topology.Order
coinduced_sup : ∀ {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {f : α → β},
  TopologicalSpace.coinduced f (t₁ ⊔ t₂) = TopologicalSpace.coinduced f t₁ ⊔ TopologicalSpace.coinduced f t₂
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.normalizerMonoidHom_ker : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G),
  H.normalizerMonoidHom.ker = (Subgroup.centralizer ↑H).subgroupOf (Subgroup.normalizer ↑H)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.range_map : ∀ {α : Type u} {β : Type v} {f : α → β},
  (FreeAddGroup.map f).range = AddSubgroup.closure (FreeAddGroup.of '' Set.range f)
-- Mathlib.Algebra.Group.Action.Units
/-- Transfer `IsScalarTower G H M` to `IsScalarTower G H Mˣ`.  -/
Units.isScalarTower' : ∀ {G : Type u_1} {H : Type u_2} {M : Type u_3} [inst : SMul G H] [inst_1 : Group G] [inst_2 : Group H]
  [inst_3 : Monoid M] [inst_4 : MulAction G M] [inst_5 : SMulCommClass G M M] [inst_6 : MulAction H M]
  [inst_7 : SMulCommClass H M M] [inst_8 : IsScalarTower G M M] [inst_9 : IsScalarTower H M M] [IsScalarTower G H M],
  IsScalarTower G H Mˣ
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.eval₂Hom_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R),
  (MvPolynomial.eval₂Hom f g) ((MvPolynomial.rename k) p) = (MvPolynomial.eval₂Hom f (g ∘ k)) p
-- Mathlib.Data.Matrix.Basis
Matrix.matrix_eq_sum_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : AddCommMonoid α] [inst_3 : Fintype m] [inst_4 : Fintype n] (x : Matrix m n α),
  x = ∑ i, ∑ j, Matrix.single i j (x i j)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h : k' ∈ Std.ExtHashMap.unitOfList l}, (Std.ExtHashMap.unitOfList l).getKey k' h = k
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.smul_assoc : ∀ {α : Type u_1} {𝕜' : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E] [inst_4 : NormedRing 𝕜'] [inst_5 : Module 𝕜' E]
  [inst_6 : Module 𝕜' 𝕜] [inst_7 : IsBoundedSMul 𝕜' E] [inst_8 : IsBoundedSMul 𝕜' 𝕜] [IsScalarTower 𝕜' 𝕜 E] (c : 𝕜')
  (f : ↥(MeasureTheory.Lp 𝕜 p μ)) (g : ↥(MeasureTheory.Lp E q μ)), (c • f) • g = c • f • g
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.mkFreshBinderName : optParam Lean.Name `x → Lean.MetavarContext.MkBinding.M Lean.Name
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (n : ℤ) (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match Lean.Grind.CommRing.Expr.num n with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_1 n
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_toArray_rio : ∀ {n : ℕ}, (*...n).toArray.toList = (*...n).toList
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List (α × β)},
  Std.HashMap.Raw.ofList l = ∅.insertMany l
-- Mathlib.Computability.Language
Symbol.terminal.injEq : ∀ {T : Type u_4} {N : Type u_5} (t t_1 : T), (Symbol.terminal t = Symbol.terminal t_1) = (t = t_1)