mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Isometry
/-- The natural isometry `∀ i, Y (e i) ≃ᵢ ∀ j, Y j` obtained from a bijection `ι ≃ ι'` of fintypes.
`Equiv.piCongrLeft` as an `IsometryEquiv`.  -/
IsometryEquiv.piCongrLeft : {ι : Type u_2} →
  {ι' : Type u_3} →
    [inst : Fintype ι] →
      [inst_1 : Fintype ι'] →
        {Y : ι' → Type u_4} →
          [inst_2 : (j : ι') → PseudoEMetricSpace (Y j)] → (e : ι ≃ ι') → ((i : ι) → Y (e i)) ≃ᵢ ((j : ι') → Y j)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_ite_irrel : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (p : Prop) [inst_1 : Decidable p] (s : Finset ι) (f g : ι → M),
  (∑ x ∈ s, if p then f x else g x) = if p then ∑ x ∈ s, f x else ∑ x ∈ s, g x
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- A point in the antidiagonal is determined by its second coordinate.

See also `Finset.antidiagonal_congr`.  -/
Finset.HasAntidiagonal.antidiagonal_congr' : ∀ {A : Type u_1} [inst : AddCancelCommMonoid A] [inst_1 : Finset.HasAntidiagonal A] {p q : A × A} {n : A},
  p ∈ Finset.HasAntidiagonal.antidiagonal n → q ∈ Finset.HasAntidiagonal.antidiagonal n → (p = q ↔ p.2 = q.2)
-- Mathlib.Data.Set.Image
/-- A variant of `image_comp`, useful for rewriting  -/
Set.image_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (s : Set α),
  g '' f '' s = (fun x => g (f x)) '' s
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listEncode.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (φ : L.BoundedFormula α (x + 1)),
  φ.all.listEncode = Sum.inr (Sum.inr 1) :: φ.listEncode
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.isUnit_det_of_invertible : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [Invertible A], IsUnit A.det
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.category : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₂} D] →
      (F : C → D) →
        (P : CategoryTheory.MorphismProperty D) →
          [inst_1 : P.IsMultiplicative] → CategoryTheory.Category.{v₁, u₁} (CategoryTheory.InducedWideCategory D F P)
-- Mathlib.GroupTheory.OrderOfElement
infinite_multiples : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {a : G}, (↑(AddSubmonoid.multiples a)).Infinite ↔ ¬IsOfFinAddOrder a
-- Mathlib.Topology.Order.LocalExtr
/-- `IsLocalMaxOn f s a` means that `f x ≤ f a` for all `x ∈ s` in some neighborhood of `a`.  -/
IsLocalMaxOn : {α : Type u} → {β : Type v} → [TopologicalSpace α] → [Preorder β] → (α → β) → Set α → α → Prop
-- Mathlib.Data.Real.Basic
Real.instDivisionRing : DivisionRing ℝ
-- Mathlib.Order.Heyting.Basic
Pi.instBiheytingAlgebra : {ι : Type u_1} → {α : ι → Type u_4} → [(i : ι) → BiheytingAlgebra (α i)] → BiheytingAlgebra ((i : ι) → α i)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The boundary of a cell is contained in a finite union of closed cells of a lower dimension.
Use `CWComplex.mapsTo` or `CWComplex.cellFrontier_subset_finite_closedCell` instead.  -/
Topology.CWComplex.mapsTo' : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C] (n : ℕ)
  (i : Topology.CWComplex.cell C n),
  ∃ I,
    Set.MapsTo (↑(Topology.CWComplex.map n i)) (Metric.sphere 0 1)
      (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(Topology.CWComplex.map m j) '' Metric.closedBall 0 1)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.of_append_right : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w}, (p.append q).IsPath → q.IsPath
-- Mathlib.Data.List.Perm.Basic
List.Perm.foldr_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {l₁ l₂ : List α} [lcomm : LeftCommutative f],
  l₁.Perm l₂ → ∀ (b : β), List.foldr f b l₁ = List.foldr f b l₂
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_self_eq_norm_sq : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), inner ℝ x x = ‖x‖ ^ 2
-- Init.Data.Slice.Array.Lemmas
Subarray.length_toList : ∀ {α : Type u_1} {xs : Subarray α}, (Std.Slice.toList xs).length = Std.Slice.size xs
-- Mathlib.Algebra.Regular.Basic
/-- An element is add-left-regular if and only if adding to it on the
left an add-left-regular element is add-left-regular.  -/
add_isAddLeftRegular_iff : ∀ {R : Type u_1} [inst : AddSemigroup R] {a : R} (b : R),
  IsAddLeftRegular a → (IsAddLeftRegular (a + b) ↔ IsAddLeftRegular b)
-- Mathlib.Data.Sigma.Interval
Sigma.instLocallyFiniteOrderTop : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Preorder (α i)] → [(i : ι) → LocallyFiniteOrderTop (α i)] → LocallyFiniteOrderTop ((i : ι) × α i)
-- Std.Time.Date.Unit.Week
Std.Time.Week.instTransOrdOffset : Std.TransOrd Std.Time.Week.Offset
-- Mathlib.Algebra.Field.Subfield.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
Subfield.gi : (K : Type u) → [inst : DivisionRing K] → GaloisInsertion Subfield.closure SetLike.coe
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.sin_eq_neg_one_iff : ∀ {x : ℝ}, Real.sin x = -1 ↔ ∃ k, -(Real.pi / 2) + ↑k * (2 * Real.pi) = x
-- Init.Data.List.Lemmas
List.getElem!_cons_succ : ∀ {α : Type u_1} {a : α} {i : ℕ} [inst : Inhabited α] {l : List α}, (a :: l)[i + 1]! = l[i]!
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.NoetherianSpace.compactSpace : ∀ (α : Type u_1) [inst : TopologicalSpace α] [h : TopologicalSpace.NoetherianSpace α], CompactSpace α
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- `toΓSpecFun` is continuous.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous : ∀ (X : AlgebraicGeometry.LocallyRingedSpace), Continuous X.toΓSpecFun
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  (i : Fin (1 + 1 + 1)),
  (G.mapComposableArrowsObjMk₂Iso f g).hom.app i =
    match i with
    | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj X)
    | ⟨i.succ, hi⟩ =>
      match ⟨i, ⋯⟩ with
      | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Y)
      | ⟨1, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Z)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffVectorBundle.of_le : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] [inst_8 : NormedAddCommGroup F]
  [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  {m n : WithTop ℕ∞}, m ≤ n → ∀ [h : ContMDiffVectorBundle n F E IB], ContMDiffVectorBundle m F E IB
-- Batteries.Data.List.Basic
List.swap.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 x_2 : ℕ),
  x.swap x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, x_3 => []
    | a :: xs, 0, 0 => a :: xs
    | a :: xs, 0, i.succ => xs[i]?.getD a :: xs.set i a
    | a :: xs, i.succ, 0 => xs[i]?.getD a :: xs.set i a
    | a :: xs, i.succ, j.succ => a :: xs.swap i j
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_closure_eq : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_toArray_rco : ∀ {m n : ℤ}, (m<...n).toArray = ((m + 1)...n).toArray
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.one : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S), WittVector.mapFun (⇑f) 1 = 1
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.instCreatesLimitsOfShapeElementsπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor C (Type w)} →
      {I : Type u₁} →
        [inst_1 : CategoryTheory.Category.{v₁, u₁} I] →
          [Small.{w, u₁} I] →
            [CategoryTheory.Limits.HasLimitsOfShape I C] →
              [CategoryTheory.Limits.PreservesLimitsOfShape I A] →
                CategoryTheory.CreatesLimitsOfShape I (CategoryTheory.CategoryOfElements.π A)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
AffineSubspace.direction_shift : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] (s : AffineSubspace k P) (c : P) (r : k), (s.shift c r).direction = s.direction
-- Mathlib.Algebra.Module.Presentation.Tautological
/-- Solutions of `tautologicalRelations A M` in an `A`-module `N` identify to `M →ₗ[A] N`.  -/
Module.Presentation.tautologicalRelationsSolutionEquiv : {A : Type u} →
  [inst : Ring A] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module A M] →
          {N : Type w} →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module A N] → (Module.Presentation.tautologicalRelations A M).Solution N ≃ (M →ₗ[A] N)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.map_apply_of : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {G' : ι → Type u_5} [inst_5 : (i : ι) → AddCommMonoid (G' i)]
  [inst_6 : (i : ι) → Module R (G' i)] {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} (g : (i : ι) → G i →ₗ[R] G' i)
  (hg : ∀ (i j : ι) (h : i ≤ j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i) {i : ι} (x : G i),
  (Module.DirectLimit.map g hg) ((Module.DirectLimit.of R ι G f i) x) = (Module.DirectLimit.of R ι G' f' i) ((g i) x)
-- Mathlib.Order.CompleteLattice.Basic
biInf_lt_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : LT ι] [NoMaxOrder ι] {f : ι → α},
  ⨅ i, ⨅ j, ⨅ (_ : j < i), f j = ⨅ i, f i
-- Mathlib.Topology.ClusterPt
/-- **Alias** of the reverse direction of `mem_closure_iff_clusterPt`. -/
ClusterPt.mem_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, ClusterPt x (Filter.principal s) → x ∈ closure s
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_zero : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Zero α], (equivShrink α).symm 0 = 0
-- Mathlib.Algebra.Star.Module
/-- Note that this lemma holds for an arbitrary `ℚ`-action, rather than merely one coming from a
`DivisionRing`. We keep both the `qsmul` and `rat_smul` naming conventions for
discoverability. See `star_rat_smul`.  -/
star_qsmul : ∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : StarAddMonoid R] [inst_2 : Module ℚ R] (q : ℚ) (x : R),
  star (q • x) = q • star x
-- Mathlib.Data.Nat.Find
Nat.find_lt_iff : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (n : ℕ), Nat.find h < n ↔ ∃ m < n, p m
-- Lean.Message
Lean.SerialMessage.mk.sizeOf_spec : ∀ (toBaseMessage : Lean.BaseMessage String) (kind : Lean.Name),
  sizeOf { toBaseMessage := toBaseMessage, kind := kind } = 1 + sizeOf toBaseMessage + sizeOf kind
-- Mathlib.AlgebraicTopology.DoldKan.Projections
/-- `Q q` is the complement projection associated to `P q`  -/
AlgebraicTopology.DoldKan.Q : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        ℕ → (AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X)
-- Mathlib.Topology.Algebra.Field
Subfield.continuousSMul : ∀ {F : Type u_2} [inst : DivisionRing F] [inst_1 : TopologicalSpace F] (X : Type u_3) [inst_2 : TopologicalSpace X]
  [inst_3 : MulAction F X] [ContinuousSMul F X] (M : Subfield F), ContinuousSMul (↥M) X
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DHashMap.Raw.Const.get! (m₁ ∪ m₂) k = Std.DHashMap.Raw.Const.getD m₂ k (Std.DHashMap.Raw.Const.get! m₁ k)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty_diff_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Mathlib.CategoryTheory.Action.Continuous
/-- Continuous version of `Functor.mapActionCongr`.  -/
CategoryTheory.Functor.mapContActionCongr : {V : Type u_5} →
  {W : Type u_6} →
    [inst : CategoryTheory.Category.{v_2, u_5} V] →
      {FV : V → V → Type u_7} →
        {CV : V → Type u_8} →
          [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory V FV] →
              [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
                [inst_4 : CategoryTheory.Category.{v_3, u_6} W] →
                  {FW : W → W → Type u_9} →
                    {CW : W → Type u_10} →
                      [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] →
                        [inst_6 : CategoryTheory.ConcreteCategory W FW] →
                          [inst_7 : CategoryTheory.HasForget₂ W TopCat] →
                            (G : Type u_11) →
                              [inst_8 : Monoid G] →
                                [inst_9 : TopologicalSpace G] →
                                  {F F' : CategoryTheory.Functor V W} →
                                    (F ≅ F') →
                                      (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) →
                                        (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous) →
                                          CategoryTheory.Functor.mapContAction G F H ≅
                                            CategoryTheory.Functor.mapContAction G F' H'
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_smul : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
    ∀ (a : ℂ), UpperHalfPlane.qExpansion h (a • f) = a • UpperHalfPlane.qExpansion h f
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instZSMul.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → SubNegMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubgroupClass (S i) (R i)],
  RestrictedProduct.instZSMul R = { smul := fun n x => ⟨fun i => n • x i, ⋯⟩ }
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_comp_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] P),
  LinearMap.lTensor N f ∘ₗ ↑(TensorProduct.comm R M N) = ↑(TensorProduct.comm R P N) ∘ₗ LinearMap.rTensor N f
-- Mathlib.Order.Hom.Lex
RelIso.sumLexComplLeft_apply : ∀ {α : Type u_1} {r : α → α → Prop} {x : α} [inst : IsTrans α r] [inst_1 : Std.Trichotomous r] [inst_2 : DecidableRel r]
  (a : { x_1 // r x_1 x } ⊕ { x_1 // ¬r x_1 x }), (RelIso.sumLexComplLeft r x) a = (Equiv.sumCompl fun x_1 => r x_1 x) a
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprLevel_mathlib.toExpr : Lean.Level → Lean.Expr
-- Init.Data.UInt.Lemmas
UInt16.toFin_val : ∀ (x : UInt16), ↑x.toFin = x.toNat
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.json : Lean.Json.CompressWorkItemKind✝
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L),
  CategoryTheory.CategoryStruct.comp (φ.map L hL) (L.map φ.s) = L.map φ.f
-- Init.Data.UInt.Lemmas
USize.div_one : ∀ {a : USize}, a / 1 = a
-- Init.Data.List.Erase
List.erase_subset : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, l.erase a ⊆ l
-- Mathlib.Algebra.Module.Equiv.Defs
/-- `e₁ ≪≫ₗ e₂` denotes the composition of the linear equivalences `e₁` and `e₂`.  -/
LinearEquiv.transNotation : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.associator_hom_apply : ∀ {R : Type u} [inst : CommSemiring R] {M N K : SemimoduleCat R} (m : ↑M) (n : ↑N) (k : ↑K),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom)
      (m ⊗ₜ[R] n ⊗ₜ[R] k) =
    m ⊗ₜ[R] (n ⊗ₜ[R] k)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.trans_refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁), (p.trans (Path.refl x₁)).Homotopic p
-- Mathlib.Data.DFinsupp.Module
DFinsupp.mk_smul : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → SMulZeroClass γ (β i)] {s : Finset ι} (c : γ) (x : (i : ↑↑s) → β ↑i),
  DFinsupp.mk s (c • x) = c • DFinsupp.mk s x
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.inftyCStarRing : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NonUnitalNormedRing (B i)] [inst_1 : (i : I) → StarRing (B i)]
  [inst_2 : ∀ (i : I), NormedStarGroup (B i)] [∀ (i : I), CStarRing (B i)], CStarRing ↥(lp B ⊤)
-- Init.Grind.AC
Lean.Grind.AC.Seq.var.sizeOf_spec : ∀ (x : Lean.Grind.AC.Var), sizeOf (Lean.Grind.AC.Seq.var x) = 1 + sizeOf x
-- Std.Do.WP.SimpLemmas
Std.Do.WP.restoreM_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ρ : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α),
  (Std.Do.wp (MonadControl.restoreM x)).apply Q = fun s => (Std.Do.wp x).apply (fun a => Q.1 a s, Q.2)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_const : ∀ {𝕜 : 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] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} (c : F) {x : M}, (d[s] fun x => c) x = 0
-- Batteries.Data.Nat.Lemmas
Nat.recDiag_succ_zero : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1))
  (m : ℕ),
  Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) 0 =
    succ_zero m (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m 0)
-- Mathlib.Data.List.Sigma
List.dlookup_dedupKeys : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)),
  List.dlookup a l.dedupKeys = List.dlookup a l
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.refl : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x x
-- Mathlib.Algebra.Category.BoolRing
instBooleanRingCarrierToBddLatToBddDistLatOfAsBoolAlg : {R : Type u} →
  [inst : BooleanRing R] →
    BooleanRing ↑{ carrier := AsBoolAlg R, str := instBooleanAlgebraAsBoolAlg }.toBddDistLat.toBddLat.toLat
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.EvalConfigItem.mk : {α : Type} → (α → Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.TermElabM α) → Lean.Elab.ConfigEval.EvalConfigItem α
-- Mathlib.Tactic.Ring.RingNF
_private.Mathlib.Tactic.Ring.RingNF.0.Mathlib.Tactic.RingNF.instEvalTermRingMode.evalTerm : Lean.Term → Lean.Elab.TermElabM (Mathlib.Tactic.RingNF.RingMode × Lean.Expr)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.of_gt : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α},
  t.Bounded o₁ o₂ → Ordnode.nil.Bounded (↑x) o₂ → Ordnode.All (fun x_1 => x_1 > x) t → t.Bounded (↑x) o₂
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
/-- Two unitary elements `u` and `v` in a unital C⋆-algebra are joined by a path if the
distance between them is less than `2`.  -/
Unitary.joined : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u v : ↥(unitary A)), ‖↑v - ↑u‖ < 2 → Joined u v
-- Mathlib.Analysis.Fourier.AddCircle
AddCircle.integral_haarAddCircle : ∀ {T : ℝ} [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : AddCircle T → E}, ∫ (t : AddCircle T), f t ∂AddCircle.haarAddCircle = T⁻¹ • ∫ (t : AddCircle T), f t
-- Lean.Parser.Basic
Lean.Parser.nonReservedSymbol : String → optParam Bool false → Lean.Parser.Parser
-- Mathlib.Data.Setoid.Partition
IndexedPartition.range_piecewise : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} (f : ι → α → β),
  Set.range (hs.piecewise f) = ⋃ i, f i '' s i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor F G X).obj S = S.snd
-- Mathlib.Algebra.Quandle
UnitalShelf.toOne : {α : Type u} → [self : UnitalShelf α] → One α
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.mk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} →
                                          (toPartialEquiv : PartialEquiv M N) →
                                            IsOpen toPartialEquiv.source →
                                              IsOpen toPartialEquiv.target →
                                                ContMDiffOn I J n (↑toPartialEquiv) toPartialEquiv.source →
                                                  ContMDiffOn J I n toPartialEquiv.invFun toPartialEquiv.target →
                                                    PartialDiffeomorph I J M N n
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.complete.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Writer.State.complete = 1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrKey.e : {enodes : Lean.Meta.Grind.ENodeMap} → Lean.Meta.Grind.CongrKey enodes → Lean.Expr
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_sup_l : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  (gi : GaloisCoinsertion l u) (a b : β), u (l a ⊔ l b) = a ⊔ b
-- Init.PropLemmas
proof_irrel_heq : ∀ {p q : Prop} (hp : p) (hq : q), hp ≍ hq
-- Mathlib.Algebra.Ring.BooleanRing
instOneBool_mathlib : One Bool