mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
/-- If `M` has a finite basis and `P` is a base change of `N` to `S`,
then `M →ₗ[R] P` is a base change of `M →ₗ[R] N` to `S`.  -/
IsBaseChange.linearMapRight : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] [inst_9 : Module S P] [inst_10 : IsScalarTower R S P]
  [Module.Free R M] [Module.Finite R M] {ε : N →ₗ[R] P}, IsBaseChange S ε → IsBaseChange S (LinearMap.compRight R ε)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R →
    CircleIntegrable g c R → ∮ (z : ℂ) in C(c, R), f z - g z = (∮ (z : ℂ) in C(c, R), f z) - ∮ (z : ℂ) in C(c, R), g z
-- Mathlib.Data.List.FinRange
List.count_finRange : ∀ {n : ℕ} (a : Fin n), List.count a (List.finRange n) = 1
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
/-- Application of a `ContinuousAlternatingMap` to a constant commutes with `fderiv`.  -/
fderiv_continuousAlternatingMap_apply_const_apply : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G} [Finite ι],
  DifferentiableAt 𝕜 c x → ∀ (u : ι → F) (m : E), (fderiv 𝕜 (fun y => (c y) u) x) m = ((fderiv 𝕜 c x) m) u
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.quoteArray : {α : Type} → [Lean.Quote α] → Array α → Lean.Term
-- Mathlib.Dynamics.FixedPoints.Basic
/-- Any map `f` sends fixed points of `g ∘ f` to fixed points of `f ∘ g`.  -/
Function.mapsTo_fixedPoints_comp : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α),
  Set.MapsTo f (Function.fixedPoints (g ∘ f)) (Function.fixedPoints (f ∘ g))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Pullback of a pre-`0`-hypercover along a morphism. The components are `pullback (E.f i) f`.  -/
CategoryTheory.PreZeroHypercover.pullback₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S T : C} →
      (f : S ⟶ T) →
        (E : CategoryTheory.PreZeroHypercover T) →
          [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] → CategoryTheory.PreZeroHypercover S
-- Init.Data.BitVec.Lemmas
BitVec.smtUDiv_zero : ∀ {n : ℕ} {x : BitVec n}, x.smtUDiv 0#n = BitVec.allOnes n
-- Lean.Data.NameMap.Basic
Lean.MacroScopesView.isSuffixOf : Lean.MacroScopesView → Lean.MacroScopesView → Bool
-- Mathlib.CategoryTheory.Core
/-- The functor `functorToCore (F ⋙ H)` factors through `functorToCore H`.  -/
CategoryTheory.Core.functorToCoreCompLeftIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : Type u₂} →
      [inst_1 : CategoryTheory.Groupoid G] →
        {G' : Type u₃} →
          [inst_2 : CategoryTheory.Groupoid G'] →
            (H : CategoryTheory.Functor G C) →
              (F : CategoryTheory.Functor G' G) →
                CategoryTheory.Core.functorToCore (F.comp H) ≅ F.comp (CategoryTheory.Core.functorToCore H)
-- Mathlib.Algebra.Star.Basic
/-- Condition that star is trivial  -/
TrivialStar.star_trivial : ∀ {R : Type u} {inst : Star R} [self : TrivialStar R] (r : R), star r = r
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_add : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Add α] (x y : Shrink.{v, u_2} α),
  (equivShrink α).symm (x + y) = (equivShrink α).symm x + (equivShrink α).symm y
-- Std.Http.Data.Chunk
/-- Trailer headers sent after the final chunk in HTTP/1.1 chunked transfer encoding.
Per RFC 9112 §7.1.2, trailers allow the sender to include additional metadata after
the message body, such as message integrity checks or digital signatures.
 -/
Std.Http.Trailer : Type
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_image_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), IsPiSystem (Set.Ici '' s)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.range_comp_subset_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f : MeasureTheory.SimpleFunc β γ) {g : α → β} (hgm : Measurable g), (f.comp g hgm).range ⊆ f.range
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.instEssentiallySmall : ∀ {S : AlgebraicGeometry.Scheme}, CategoryTheory.EssentiallySmall.{u, u, u + 1} S.AffineEtale
-- Lean.Elab.Command
Lean.Elab.Command.instMonadDeclNameGeneratorCommandElabM : Lean.MonadDeclNameGenerator Lean.Elab.Command.CommandElabM
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.instCoeFormatterAliasValue : Coe Lean.PrettyPrinter.Formatter Lean.PrettyPrinter.Formatter.FormatterAliasValue
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.id_mapId : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : B),
  (CategoryTheory.OplaxFunctor.id B).mapId a = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
-- Mathlib.SetTheory.ZFC.Ordinal
/-- **Alias** of the forward direction of `ZFSet.isTransitive_iff_sUnion_subset`. -/
ZFSet.IsTransitive.sUnion_subset : ∀ {x : ZFSet.{u}}, x.IsTransitive → x.sUnion ⊆ x
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- A free additive group over one generator is an instance of a cyclic group.  -/
FreeGroup.instIsAddCyclicFreeAddGroupOfUnique : ∀ {α : Type u} [Unique α], IsAddCyclic (FreeAddGroup α)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.le_iff : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J J' : hI.SubDPIdeal},
  J ≤ J' ↔ J.carrier ≤ J'.carrier
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpUniqueProd_symm_apply : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Unique α] (a : β),
  (IsometryEquiv.withLpUniqueProd p α β).symm a = WithLp.toLp p (default, a)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Recursive definition of an ordinal notation. `zero` denotes the ordinal 0, and `oadd e n a` is
intended to refer to `ω ^ e * n + a`. For this to be a valid Cantor normal form, we must have the
exponents decrease to the right, but we can't state this condition until we've defined `repr`, so we
make it a separate definition `NF`.  -/
ONote : Type
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyoneda_obj_map : ∀ (M : CommGrpCatᵒᵖ) {X Y : CommGrpCat} (f : X ⟶ Y),
  (CommGrpCat.coyoneda.obj M).map f = CommGrpCat.ofHom (MonoidHom.compHom (CommGrpCat.Hom.hom f))
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.throwWrongArgCount : {α : Type} → Lean.Elab.Term.CollectPatternVars.Context → Bool → Lean.Elab.Term.CollectPatternVars.M α
-- Init.Data.String.Pattern.Basic
/-- Provides simple pattern matching capabilities from the start of a `Slice`.
 -/
String.Slice.Pattern.ForwardPattern : {ρ : Type} → ρ → Type
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.limit_one_val : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) (j : J),
  ↑1 j = 1
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.RedRed.reverse : ∀ {p : Prop} {α : Type u_1} {t : RBTree.RBNode α} {n : ℕ},
  RBTree.RBNode.RedRed p t n → RBTree.RBNode.RedRed p t.reverse n
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_eq_zero_iff : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  {I : Ideal S}, Ideal.absNorm I = 0 ↔ I = ⊥
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.keysArray_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.keysArray = t₂.keysArray
-- Mathlib.Analysis.Matrix.LDL
/-- The inverse of the lower triangular matrix `L` of the LDL-decomposition. It is obtained by
applying Gram-Schmidt-Orthogonalization w.r.t. the inner product induced by `Sᵀ` on the standard
basis vectors `Pi.basisFun`.  -/
LDL.lowerInv : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : LinearOrder n] →
        [WellFoundedLT n] → [LocallyFiniteOrderBot n] → {S : Matrix n n 𝕜} → [Fintype n] → S.PosDef → Matrix n n 𝕜
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.map f m).getKey? k = m.getKey? k
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.SigmaFinite.of_map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] (μ : MeasureTheory.Measure α)
  {f : α → β},
  AEMeasurable f μ → MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ) → MeasureTheory.SigmaFinite μ
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The composition of a rational map and a morphism on the right.  -/
AlgebraicGeometry.Scheme.RationalMap.compHom : {X Y Z : AlgebraicGeometry.Scheme} → X.RationalMap Y → (Y ⟶ Z) → X.RationalMap Z
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- **Alias** of `Finsupp.support_finsetSum`. -/
Finsupp.support_finset_sum : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} [inst : DecidableEq β] [inst_1 : AddCommMonoid M] {s : Finset α}
  {f : α → β →₀ M}, (s.sum f).support ⊆ s.biUnion fun x => (f x).support
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.map₂_leftUnitor_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (F.map f))
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f)
        (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred
Std.Tactic.BVDecide.BVPred.bitblast_denote_mem_prefix : ∀ {inv : Bool} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (start : ℕ) (hstart : start < aig.decls.size),
  ⟦assign.toAIGAssignment,
      { aig := (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Analysis.Seminorm
Seminorm.zero_comp : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (f : E →ₛₗ[σ₁₂] E₂), Seminorm.comp 0 f = 0
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.id_map : ∀ {C : CategoryTheory.Cat} {X Y : ↑C} (f : X ⟶ Y), (CategoryTheory.CategoryStruct.id C).toFunctor.map f = f
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- A fork is a limit cone if and only if the corresponding cofork in the opposite category is
a colimit cocone.  -/
CategoryTheory.Limits.Fork.isLimitEquivIsColimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        (c : CategoryTheory.Limits.Fork f g) → CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsColimit c.op
-- Lean.Elab.Tactic.Location
Lean.Elab.Tactic.Location.targets.inj : ∀ {hypotheses : Array Lean.Syntax} {type : Bool} {hypotheses_1 : Array Lean.Syntax} {type_1 : Bool},
  Lean.Elab.Tactic.Location.targets hypotheses type = Lean.Elab.Tactic.Location.targets hypotheses_1 type_1 →
    hypotheses = hypotheses_1 ∧ type = type_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) {Z : C}
  (h_1 : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g)
      (CategoryTheory.CategoryStruct.comp s.snd h_1) =
    CategoryTheory.CategoryStruct.comp g h_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_maxKey_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp k (t.maxKey ⋯)).isLE = true
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.coe_lt_coe : ∀ {E : Type u_3} [inst : Group E] {p q : GroupSeminorm E}, ⇑p < ⇑q ↔ p < q
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.loogleUsage : String
-- Mathlib.Tactic.GCongr.Core
/-- Run the discharger for side goals.  -/
Mathlib.Tactic.GCongr.dischargeSide : Lean.MVarId → Mathlib.Tactic.GCongr.GCongrM Unit
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.mem_toPointedCone : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] {C : ProperCone R E} {x : E},
  x ∈ ↑C ↔ x ∈ C
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.toRuleBuilder : Aesop.Frontend.DBuilderName → Aesop.RuleBuilder
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.braiding'_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C),
  (CategoryTheory.Limits.biprod.braiding' P Q).inv =
    CategoryTheory.Limits.biprod.desc CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.inl
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLeftStrictMono.toIsLeftCancelAdd : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] [AddLeftStrictMono α], IsLeftCancelAdd α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = false → m.getKey? a = none
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.terminal.strict_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] {A : C} (f g : ⊤_ C ⟶ A), f = g
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- **Alias** of `MeasureTheory.locallyIntegrable_finsetSum'`. -/
MeasureTheory.locallyIntegrable_finset_sum' : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  {ε''' : Type u_9} [inst_2 : TopologicalSpace ε'''] [inst_3 : ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε''']
  {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''},
  (∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ) → MeasureTheory.LocallyIntegrable (∑ i ∈ s, f i) μ
-- Mathlib.RingTheory.FiniteType
/-- If a set `S` generates a monoid `M`, then the image of `M` generates, as algebra,
`R[M]`.  -/
MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure : ∀ {R : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : CommSemiring R] {S : Set M},
  Submonoid.closure S = ⊤ → Function.Surjective ⇑(MvPolynomial.aeval fun s => (MonoidAlgebra.of R M) ↑s)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW_iff_of_distinguished : ∀ {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]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P.trW T.mor₁ ↔ P T.obj₃
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.match_1.eq_1 : ∀ (motive : Lean.Expr → Sort u_1) (a : Lean.Literal) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (f a : Lean.Expr) → motive (f.app a))
  (h_8 : (data : Lean.MData) → (a : Lean.Expr) → motive (Lean.Expr.mdata data a))
  (h_9 : (typeName : Lean.Name) → (idx : ℕ) → (a : Lean.Expr) → motive (Lean.Expr.proj typeName idx a))
  (h_10 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName d b binderInfo))
  (h_11 :
    (binderName : Lean.Name) →
      (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.lam binderName d b binderInfo))
  (h_12 :
    (declName : Lean.Name) → (t v b : Lean.Expr) → (nondep : Bool) → motive (Lean.Expr.letE declName t v b nondep)),
  (match Lean.Expr.lit a with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | f.app a => h_7 f a
    | Lean.Expr.mdata data a => h_8 data a
    | Lean.Expr.proj typeName idx a => h_9 typeName idx a
    | Lean.Expr.forallE binderName d b binderInfo => h_10 binderName d b binderInfo
    | Lean.Expr.lam binderName d b binderInfo => h_11 binderName d b binderInfo
    | Lean.Expr.letE declName t v b nondep => h_12 declName t v b nondep) =
    h_1 a
-- Init.Grind.Lemmas
Lean.Grind.Semiring.one_mul_congr : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] {a b : α}, a = 1 → a * b = b
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.equivalence_counitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (x : ULift.{u₂, u₁} C),
  CategoryTheory.ULift.equivalence.counitIso.inv.app x =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (ULift.{u₂, u₁} C)).obj x)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
notMem_nonZeroDivisorsRight_iff : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] {x : M₀}, x ∉ nonZeroDivisorsRight M₀ ↔ {y | y * x = 0 ∧ y ≠ 0}.Nonempty
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mk_sub_mk : ∀ {R : Type u_1} {a b : R} [inst : Sub R] (x1 y1 x2 y2 : R),
  { re := x1, im := y1 } - { re := x2, im := y2 } = { re := x1 - x2, im := y1 - y2 }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (fallback fallback_1 : β), fallback = fallback_1 → t.getD a fallback = t_1.getD a_1 fallback_1
-- Lean.Elab.Tactic.Omega.Frontend
Lean.Elab.Tactic.Omega.MetaProblem.mk.inj : ∀ {problem : Lean.Elab.Tactic.Omega.Problem} {facts disjunctions : List Lean.Expr}
  {processedFacts : Std.HashSet Lean.Expr} {problem_1 : Lean.Elab.Tactic.Omega.Problem}
  {facts_1 disjunctions_1 : List Lean.Expr} {processedFacts_1 : Std.HashSet Lean.Expr},
  { problem := problem, facts := facts, disjunctions := disjunctions, processedFacts := processedFacts } =
      { problem := problem_1, facts := facts_1, disjunctions := disjunctions_1, processedFacts := processedFacts_1 } →
    problem = problem_1 ∧ facts = facts_1 ∧ disjunctions = disjunctions_1 ∧ processedFacts = processedFacts_1
-- Mathlib.Analysis.Normed.Lp.lpSpace
algebraMap_memℓp_infty : ∀ {𝕜 : Type u_1} {I : Type u_5} {B : I → Type u_6} [inst : NormedField 𝕜] [inst_1 : (i : I) → NormedRing (B i)]
  [inst_2 : (i : I) → NormedAlgebra 𝕜 (B i)] [∀ (i : I), NormOneClass (B i)] (k : 𝕜),
  Memℓp ((algebraMap 𝕜 ((i : I) → B i)) k) ⊤
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.forget_ε : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Center.forget C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_of_sum_add_sum_eq_zero : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {w : ι → R} {z : ι → E} {s t : Finset ι},
  ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0 → ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0 → s.centerMass w z = t.centerMass w z
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_lt_iff : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ k, p k) (i : Fin n), Fin.find p h < i ↔ ∃ m < i, p m
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.restrictPreimage'_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) (s : Set B) [inst_2 : Nonempty (↑s → F → ↑(proj ⁻¹' s))],
  (e.restrictPreimage' s).source = Subtype.val ⁻¹' e.source
-- Init.Data.List.Basic
/-- If `l₁` is a subsequence of `l₂`, then `a :: l₁` is a subsequence of `a :: l₂`.  -/
List.Sublist.cons_cons : ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → (a :: l₁).Sublist (a :: l₂)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.lift_symm_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] (f : FreeAddMonoid α →+ M),
  FreeAddMonoid.lift.symm f = ⇑f ∘ FreeAddMonoid.of
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.NatTrans.mapHomotopyCategory_app : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W] [inst_3 : CategoryTheory.Preadditive W]
  {F G : CategoryTheory.Functor V W} [inst_4 : F.Additive] [inst_5 : G.Additive] (α : F ⟶ G) (c : ComplexShape ι)
  (C : HomotopyCategory V c),
  (CategoryTheory.NatTrans.mapHomotopyCategory α c).app C =
    (HomotopyCategory.quotient W c).map ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C.as)
-- Mathlib.Data.ENNReal.Basic
ENNReal.instCanonicallyOrderedAdd : CanonicallyOrderedAdd ENNReal
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.toComplex_inj : ∀ {x y : GaussianInt}, GaussianInt.toComplex x = GaussianInt.toComplex y ↔ x = y
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.sdiv : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β}, s.Nonempty → t.Nonempty → (s /ₛ t).Nonempty
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.HasLeftDerivedFunctor.mk' : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) {W : CategoryTheory.MorphismProperty C} [inst_3 : L.IsLocalization W]
  [LF.IsLeftDerivedFunctor α W], F.HasLeftDerivedFunctor W
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff.sizeOf_spec : ∀ (R : Type u_1) {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : SizeOf R]
  [inst_4 : SizeOf M] (coeff : ℕ →₀ M), sizeOf { coeff := coeff } = 1 + sizeOf coeff
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_sep : ∀ (a : ZFSet.{u_1}) (p : ZFSet.{u_1} → Prop), ↑(ZFSet.sep p a) = {x | x ∈ a ∧ p x}