mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_eq_lintegral_mfderiv_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M},
  Manifold.pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Icc a b, ‖(mfderiv% γ t) 1‖ₑ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfLeftIso_x : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f], (CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).pt = Z
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.congrLeft` as a `RingEquiv`.  -/
LocallyConstant.congrLeftRingEquiv : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} → [inst_2 : Semiring Z] → X ≃ₜ Y → LocallyConstant X Z ≃+* LocallyConstant Y Z
-- Mathlib.Data.UInt
UInt8.toBitVec_zsmul : ∀ (z : ℤ) (a : UInt8), (z • a).toBitVec = z • a.toBitVec
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.isTriangulated_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {E : Type u_3} [inst_6 : CategoryTheory.Category.{v_3, u_3} E] [inst_7 : CategoryTheory.HasShift E ℤ]
  (P : CategoryTheory.ObjectProperty C) [inst_8 : P.IsTriangulated] (F : CategoryTheory.Functor E C)
  (hF : ∀ (X : E), P (F.obj X)) [inst_9 : CategoryTheory.Preadditive E] [inst_10 : F.CommShift ℤ]
  [inst_11 : CategoryTheory.Limits.HasZeroObject E] [inst_12 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive]
  [inst_13 : CategoryTheory.Pretriangulated E] [F.IsTriangulated], (P.lift F hF).IsTriangulated
-- Mathlib.CategoryTheory.Abelian.Indization
CategoryTheory.instAbelianInd : {C : Type v} →
  [inst : CategoryTheory.SmallCategory C] → [CategoryTheory.Abelian C] → CategoryTheory.Abelian (CategoryTheory.Ind C)
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.mkOfClosure_eq_generateFrom : ∀ {X : Type u_1} {g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))}
  {hg : (DiffeologicalSpace.generateFrom g).toPlots = g},
  DiffeologicalSpace.mkOfClosure g hg = DiffeologicalSpace.generateFrom g
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.leftUnitor_hom_apply : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} (r : R) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom) (r ⊗ₜ[R] m) = r • m
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_rightUnitor_inv_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} (f : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor f).inv.unop2 = (CategoryTheory.Bicategory.leftUnitor f.unop).inv
-- Mathlib.Data.Finset.Range
coe_notMemRangeEquiv : ∀ (k : ℕ), ⇑(notMemRangeEquiv k) = fun i => ↑i - k
-- Aesop.Script.Step
Aesop.Script.LazyStep.mk.inj : ∀ {preState : Lean.Meta.SavedState} {preGoal : Lean.MVarId} {tacticBuilders : Array Aesop.Script.TacticBuilder}
  {tacticBuilders_ne : autoParam (0 < tacticBuilders.size) Aesop.Script.LazyStep.tacticBuilders_ne._autoParam}
  {postState : Lean.Meta.SavedState} {postGoals : Array Lean.MVarId} {preState_1 : Lean.Meta.SavedState}
  {preGoal_1 : Lean.MVarId} {tacticBuilders_1 : Array Aesop.Script.TacticBuilder}
  {tacticBuilders_ne_1 : autoParam (0 < tacticBuilders_1.size) Aesop.Script.LazyStep.tacticBuilders_ne._autoParam}
  {postState_1 : Lean.Meta.SavedState} {postGoals_1 : Array Lean.MVarId},
  { preState := preState, preGoal := preGoal, tacticBuilders := tacticBuilders, tacticBuilders_ne := tacticBuilders_ne,
        postState := postState, postGoals := postGoals } =
      { preState := preState_1, preGoal := preGoal_1, tacticBuilders := tacticBuilders_1,
        tacticBuilders_ne := tacticBuilders_ne_1, postState := postState_1, postGoals := postGoals_1 } →
    preState = preState_1 ∧
      preGoal = preGoal_1 ∧ tacticBuilders = tacticBuilders_1 ∧ postState = postState_1 ∧ postGoals = postGoals_1
-- Mathlib.Order.Heyting.Basic
Disjoint.sdiff_eq_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → b \ a = b
-- Lean.DocString.DeferredCheck
Lean.Doc.instBEqDeferredCheckSite : BEq Lean.Doc.DeferredCheckSite
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {l : List ((a : α) × β a)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (↑(t.insertMany l ⋯)).getKey? k' = some k
-- Mathlib.CategoryTheory.Join.Sum
_private.Mathlib.CategoryTheory.Join.Sum.0.CategoryTheory.sum.match_3.eq_1 : ∀ (C : Type u_1) (D : Type u_2) (motive : C ⊕ D → Sort u_3) (X : C) (h_1 : (X : C) → motive (Sum.inl X))
  (h_2 : (X : D) → motive (Sum.inr X)),
  (match Sum.inl X with
    | Sum.inl X => h_1 X
    | Sum.inr X => h_2 X) =
    h_1 X
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.eval_obj : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) (f : (i : I) → C i),
  (CategoryTheory.Pi.eval C i).obj f = f i
-- Init.Data.SInt.Basic
/-- Converts a 64-bit signed integer to a 32-bit signed integer by truncating its bitvector
representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.toInt32 : Int64 → Int32
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k fallback : α}, t.WF → (Std.TreeMap.Raw.map f t).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.instIsDominantHomToPartialMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsDominant f],
  AlgebraicGeometry.IsDominant (AlgebraicGeometry.Scheme.Hom.toPartialMap f).hom
-- Mathlib.Order.SuccPred.Basic
/-- Order equipped with a sensible successor function.  -/
SuccOrder : (α : Type u_3) → [Preorder α] → Type u_3
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A translate of a block is a block  -/
MulAction.IsBlock.translate : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X} (g : G),
  MulAction.IsBlock G B → MulAction.IsBlock G (g • B)
-- Mathlib.LinearAlgebra.Charpoly.BaseChange
LinearMap.det_eq_sign_charpoly_coeff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M),
  LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.sumCoords.eq_1 : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), b.sumCoords = ((Finsupp.lsum ℕ) fun x => LinearMap.id) ∘ₗ ↑b.repr
-- Init.Tactics
/-- The common arguments of `simp?` and `simp?!`.  -/
Lean.Parser.Tactic.simpTraceArgsRest : Lean.ParserDescr
-- Lean.Compiler.LCNF.PublicDeclsExt
/-- Set of declarations to be exported to other modules; visibility shared by base/mono/IR phases.
 -/
_private.Lean.Compiler.LCNF.PublicDeclsExt.0.Lean.Compiler.LCNF.publicDeclsExt : Lean.EnvExtension (List Lean.Name × Lean.NameSet)
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.instHasSheafifyType : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  CategoryTheory.HasSheafify J (Type (max u v))
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.colex_lt_iff_of_unique : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : Unique ι] [inst_2 : (i : ι) → LT (α i)]
  [inst_3 : Preorder ι] {x y : Colex (Π₀ (i : ι), α i)}, x < y ↔ (ofColex x) default < (ofColex y) default
-- Init.Data.Int.Gcd
Int.gcd_pos_of_ne_zero_right : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → 0 < a.gcd b
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.IsUltra.le_sup : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] [inst_3 : Max R] {d : PseudoMetric X R}
  [hd : d.IsUltra] {x y z : X}, d x z ≤ d x y ⊔ d y z
-- Lean.Meta.Basic
/-- Not `none` when inside of an `isDefEq` test. See `PostponedEntry`.  -/
Lean.Meta.Context.defEqCtx? : Lean.Meta.Context → Option Lean.Meta.DefEqContext
-- Mathlib.Order.SupIndep
Finset.SupIndep.subset : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s t : Finset ι} {f : ι → α},
  t.SupIndep f → s ⊆ t → s.SupIndep f
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.mul_comm_iff : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] [IsScalarTower S A A] [SMulCommClass S A A]
  {f : S → R} {a b : A}, QuasispectrumRestricts (a * b) f ↔ QuasispectrumRestricts (b * a) f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_id : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (s : AffineSubspace k P₁), AffineSubspace.comap (AffineMap.id k P₁) s = s
-- Init.Data.Nat.Basic
Nat.add_one_ne_self : ∀ (n : ℕ), n + 1 ≠ n
-- Std.Time.DateTime.Timestamp
/-- Adds a `Second.Offset` to the given `Timestamp`.
 -/
Std.Time.Timestamp.addSeconds : Std.Time.Timestamp → Std.Time.Second.Offset → Std.Time.Timestamp
-- Lean.Meta.Tactic.Grind.Types
/-- Returns node associated with `e`. It assumes `e` has already been internalized.  -/
Lean.Meta.Grind.Goal.getENode : Lean.Meta.Grind.Goal → Lean.Expr → Lean.MetaM Lean.Meta.Grind.ENode
-- Mathlib.Order.UpperLower.Basic
isLowerSet_Iic : ∀ {α : Type u_1} [inst : Preorder α] (a : α), IsLowerSet (Set.Iic a)
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.instCategory : {X Y : CategoryTheory.Cat} → CategoryTheory.Category.{max u v, max u v} (X ⟶ Y)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.norm_exp_I_mul_ofReal_sub_one : ∀ (x : ℝ), ‖Complex.exp (Complex.I * ↑x) - 1‖ = ‖2 * Real.sin (x / 2)‖
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The precomposition of a cocycle with a morphism of cochain complexes.  -/
CochainComplex.HomComplex.Cocycle.precomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G K : CochainComplex C ℤ} →
        {n : ℤ} → CochainComplex.HomComplex.Cocycle G K n → (F ⟶ G) → CochainComplex.HomComplex.Cocycle F K n
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.full_constantSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [CategoryTheory.LocallySmall.{w, v, u} C] [J.IsLocalSite] (A : Type u') [inst_3 : CategoryTheory.Category.{v', u'} A]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.Limits.HasProducts A]
  [inst_6 : CategoryTheory.HasWeakSheafify J A], (CategoryTheory.constantSheaf J A).Full
-- Mathlib.CategoryTheory.Subterminal
/-- If `A` is subterminal, it is isomorphic to `A ⨯ A`.  -/
CategoryTheory.IsSubterminal.isoDiag : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : C} → CategoryTheory.IsSubterminal A → [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A] → A ⨯ A ≅ A
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherian_of_le : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s t : Submodule R M} [ht : IsNoetherian R ↥t], s ≤ t → IsNoetherian R ↥s
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_lt_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  Int.fract a < 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.isNormalHom_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] {φ : H ⟶ G}
  [CategoryTheory.IsMonHom φ] [CategoryTheory.Mono φ],
  CategoryTheory.IsMonHom.Normal φ ↔
    ∃ ψ,
      CategoryTheory.CategoryStruct.comp ψ φ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ)
          (CategoryTheory.GrpObj.conj G)
-- Mathlib.Data.Set.Prod
Set.diagonal_eq_univ : ∀ {α : Type u_1} [Subsingleton α], Set.diagonal α = Set.univ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.DTreeMap.Raw.ofList l cmp).getD k' fallback = cast ⋯ v
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofBijective.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f f_1 : M →ₛₗ[σ₁₂] M₂) (e_f : f = f_1) [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] (hf : Function.Bijective ⇑f),
  LinearEquiv.ofBijective f hf = LinearEquiv.ofBijective f_1 ⋯
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom =
          CategoryTheory.CategoryStruct.comp (app X).hom (G.map f))
      CategoryTheory.NatIso.ofComponents._auto_1)
  (X : C), (CategoryTheory.NatIso.ofComponents app naturality).hom.app X = (app X).hom
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacticM.inj : ∀ {decl decl_1 : Lean.Name}, Aesop.RuleTacDescr.tacticM decl = Aesop.RuleTacDescr.tacticM decl_1 → decl = decl_1
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} [inst_1 : SizeOf C]
  (obj : (U : C) → Set (F.obj U))
  (map : ∀ {U V : C} (i : U ⟶ V), obj U ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map i)) ⁻¹' obj V),
  sizeOf { obj := obj, map := map } = 1
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.instCategory : CategoryTheory.Category.{w, w + 1} CompactlyGenerated
-- Mathlib.Data.Option.NAry
Option.map₂_some_some : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β),
  Option.map₂ f (some a) (some b) = some (f a b)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], ∅.min? = none
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppEMatchTheorem : Lean.Meta.Grind.EMatchTheorem → Lean.MetaM Lean.MessageData
-- Lean.Message
Lean.SerialMessage.toBaseMessage : Lean.SerialMessage → Lean.BaseMessage String
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.IsEquiv.map : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedAddCommMonoidWithTop Γ₀]
  [inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀] [inst_2 : Ring R] {v v' : AddValuation R Γ₀} (f : Γ₀ →+ Γ'₀)
  (ht : f ⊤ = ⊤) (hf : Monotone ⇑f),
  Function.Injective ⇑f → v.IsEquiv v' → (AddValuation.map f ht hf v).IsEquiv (AddValuation.map f ht hf v')
-- Mathlib.Analysis.Normed.Module.Complemented
/-- **Alias** of `Submodule.ClosedComplemented.of_isCompl_isClosed`. -/
Submodule.IsCompl.closedComplemented_of_isClosed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E},
  IsCompl p q → IsClosed ↑p → IsClosed ↑q → Submodule.ClosedComplemented p
-- Mathlib.Tactic.Clean
/-- `clean% t` fully elaborates `t` and then eliminates all identity functions from it.

Identity functions are normally generated with terms like `show t from p`,
which translate to some variant on `@id t p` in order to retain the type.
These are also generated by tactics such as `dsimp` to insert type hints.

Example:
```lean
def x : Id Nat := by dsimp [Id]; exact 1
#print x
-- def x : Id Nat := id 1

def x' : Id Nat := clean% by dsimp [Id]; exact 1
#print x'
-- def x' : Id Nat := 1
```
 -/
Mathlib.Tactic.elabClean : Lean.Elab.Term.TermElab
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.NormalExpr.cons.inj : ∀ {e : Mathlib.Tactic.BicategoryLike.Mor₂} {α : Mathlib.Tactic.BicategoryLike.Structural}
  {η : Mathlib.Tactic.BicategoryLike.WhiskerLeft} {ηs : Mathlib.Tactic.BicategoryLike.NormalExpr}
  {e_1 : Mathlib.Tactic.BicategoryLike.Mor₂} {α_1 : Mathlib.Tactic.BicategoryLike.Structural}
  {η_1 : Mathlib.Tactic.BicategoryLike.WhiskerLeft} {ηs_1 : Mathlib.Tactic.BicategoryLike.NormalExpr},
  Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs =
      Mathlib.Tactic.BicategoryLike.NormalExpr.cons e_1 α_1 η_1 ηs_1 →
    e = e_1 ∧ α = α_1 ∧ η = η_1 ∧ ηs = ηs_1
-- Mathlib.LinearAlgebra.CrossProduct
crossProduct_ne_zero_iff_linearIndependent : ∀ {F : Type u_2} [inst : Field F] {v w : Fin 3 → F}, (crossProduct v) w ≠ 0 ↔ LinearIndependent F ![v, w]
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [AlgebraicGeometry.IsFinite g],
  AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsFinite f
-- Lean.Parser.Basic
Lean.Parser.nonReservedSymbolFn : String → Lean.Parser.ParserFn
-- Lean.Meta.Tactic.Induction
_private.Lean.Meta.Tactic.Induction.0.Lean.Meta.finalize.loop : Lean.MVarId →
  Array Lean.Meta.AltVarNames →
    Lean.Meta.RecursorInfo →
      Array Lean.FVarId →
        Lean.Expr →
          Array Lean.Expr →
            Lean.Meta.FVarSubst →
              ℕ →
                ℕ →
                  ℕ →
                    ℕ →
                      Lean.Expr →
                        Lean.Expr →
                          Bool → Array Lean.Meta.InductionSubgoal → Lean.MetaM (Array Lean.Meta.InductionSubgoal)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
prime_factors_unique : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {f g : Multiset α},
  (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → Associated f.prod g.prod → Multiset.Rel Associated f g
-- Init.Grind.AC
Lean.Grind.AC.superpose_cert.eq_1 : ∀ (p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_cert p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs =
    (((lhs₁.beq' (p.concat_k c)).and' (lhs₂.beq' (c.concat_k s))).and' (lhs.beq' (rhs₁.concat_k s))).and'
      (rhs.beq' (p.concat_k rhs₂))
-- Lean.Parser.Basic
Lean.Syntax.foldArgs : {β : Type u_1} → Lean.Syntax → (Lean.Syntax → β → β) → β → β
-- Init.Data.List.Sublist
List.Sublist.append_right : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ (l : List α), (l₁ ++ l).Sublist (l₂ ++ l)
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_zipIdx_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β},
  xs.mapFinIdx f =
    Vector.map
      (fun x =>
        match x with
        | ⟨(x, i), m⟩ => f i x ⋯)
      xs.zipIdx.attach
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_diff_eq_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Mathlib.Topology.Category.TopCat.Sphere
/-- The boundary of the `n`-disk.  -/
TopCat.diskBoundary : ℕ → TopCat
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.Hom.eq_3 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (a : C) (a_1 : D), (CategoryTheory.Join.left a).Hom (CategoryTheory.Join.right a_1) = PUnit.{max (v₁ + 1) (v₂ + 1)}
-- Mathlib.Order.Filter.Pi
Filter.mem_pi' : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : Set ((i : ι) → α i)},
  s ∈ Filter.pi f ↔ ∃ I t, (∀ (i : ι), t i ∈ f i) ∧ (↑I).pi t ⊆ s
-- Mathlib.GroupTheory.Congruence.Basic
Con.mulAction.eq_1 : ∀ {α : Type u_4} {M : Type u_5} [inst : Monoid α] [inst_1 : MulOneClass M] [inst_2 : MulAction α M]
  [inst_3 : IsScalarTower α M M] (c : Con M), c.mulAction = { toSMul := c.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.transpose_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) (n : ℤ), (A ^ n).transpose = A.transpose ^ n
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_sieve : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.generate S.arrows = S
-- Mathlib.RingTheory.DualNumber
TrivSqZeroExt.isUnit_or_isNilpotent_of_isMaximal_isNilpotent : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [inst_4 : IsCentralScalar R M],
  (∀ (I : Ideal R), I.IsMaximal → IsNilpotent I) → ∀ (a : TrivSqZeroExt R M), IsUnit a ∨ IsNilpotent a
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- An integral domain is equal to the intersection of its localizations at all its prime ideals
viewed as subalgebras of its field of fractions.  -/
PrimeSpectrum.iInf_localization_eq_bot : ∀ (R : Type u_4) [inst : CommRing R] [inst_1 : IsDomain R] (K : Type u_5) [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K], ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ = ⊥
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalGroup.mulInvClosureNhd.isOpen : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : Group G],
  IsTopologicalGroup.mulInvClosureNhd T W → IsOpen T
-- Batteries.Data.List.Perm
List.Perm.subperm_right : ∀ {α : Type u_1} {l₁ l₂ l : List α}, l₁.Perm l₂ → (l₁.Subperm l ↔ l₂.Subperm l)
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_leOnePart_injective : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α], Function.Injective fun a => (a⁺ᵐ, a⁻ᵐ)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_finsetSum' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n (∑ i ∈ t, f i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.eval_mul : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinOp.mul.eval = fun x1 x2 => x1 * x2
-- Lean.Util.MonadBacktrack
Lean.instMonadBacktrackExceptTOfMonad : {s : Type} →
  {m : Type → Type} → {ε : Type} → [Lean.MonadBacktrack s m] → [Monad m] → Lean.MonadBacktrack s (ExceptT ε m)
-- Std.Http.Test.Helpers
Std.Http.Internal.Test.r431 : String