mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.Fib.mkIsoSelfIsHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a : 𝒳} (ha : p.obj a = S),
  p.IsHomLift (CategoryTheory.CategoryStruct.id S) (HasFibers.Fib.mkIsoSelf ha).hom
-- Mathlib.Data.Rat.Cast.CharZero
Rat.coe_castHom : ∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α], ⇑(Rat.castHom α) = Rat.cast
-- Mathlib.GroupTheory.IsSubnormal
/-- The image of a subnormal additive subgroup under a surjective homomorphism is subnormal.  -/
AddSubgroup.IsSubnormal.map : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {G' : Type u_2} [inst_1 : AddGroup G'] {f : G →+ G'},
  Function.Surjective ⇑f → H.IsSubnormal → (AddSubgroup.map f H).IsSubnormal
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDistribMulActionAddMonoidHom : {A : Type u_5} →
  {M : Type u_6} →
    {B : Type u_7} →
      [inst : Monoid M] →
        [inst_1 : AddMonoid A] → [DistribMulAction M A] → [inst_3 : AddCommMonoid B] → DistribMulAction Mᵈᵐᵃ (A →+ B)
-- Lean.Data.Json.Basic
Lean.JsonNumber.fromInt : ℤ → Lean.JsonNumber
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → ∀ {h' : k' ∈ Std.ExtTreeSet.ofList l cmp}, (Std.ExtTreeSet.ofList l cmp).get k' h' = k
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.mk.inj : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {inst : NontriviallyNormedField 𝕜} {inst_1 : AddCommGroup E}
  {inst_2 : AddCommGroup F} {inst_3 : Module 𝕜 E} {inst_4 : Module 𝕜 F} {inst_5 : TopologicalSpace E}
  {inst_6 : TopologicalSpace F} {u : E →L[𝕜] F} {decDom : FredholmDecomposition 𝕜 E}
  {decCodom : FredholmDecomposition 𝕜 F} {equiv : ↥decDom.X₁ ≃L[𝕜] ↥decCodom.X₁}
  {eq_equiv : u = decCodom.X₁.subtypeL ∘SL ↑equiv ∘SL decDom.proj} {decDom_1 : FredholmDecomposition 𝕜 E}
  {decCodom_1 : FredholmDecomposition 𝕜 F} {equiv_1 : ↥decDom_1.X₁ ≃L[𝕜] ↥decCodom_1.X₁}
  {eq_equiv_1 : u = decCodom_1.X₁.subtypeL ∘SL ↑equiv_1 ∘SL decDom_1.proj},
  { decDom := decDom, decCodom := decCodom, equiv := equiv, eq_equiv := eq_equiv } =
      { decDom := decDom_1, decCodom := decCodom_1, equiv := equiv_1, eq_equiv := eq_equiv_1 } →
    decDom = decDom_1 ∧ decCodom = decCodom_1 ∧ equiv ≍ equiv_1
-- Init.Notation
/-- Boolean negation, also known as Boolean complement. `not x` can be written `!x`.

This is a function that maps the value `true` to `false` and the value `false` to `true`. The
propositional connective is `Not : Prop → Prop`.


Conventions for notations in identifiers:

 * The recommended spelling of `!` in identifiers is `not`. -/
term!_ : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.ne_push_self : ∀ {α : Type u_1} {a : α} {xs : Array α}, xs ≠ xs.push a
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.prop : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α), Heyting.IsRegular ↑a
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_ne_zero : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane), UpperHalfPlane.denom g ↑z ≠ 0
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.mapAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_6} [inst_1 : AddGroup H] (f : G ≃+ H),
  f.mapAddSubgroup =
    { toFun := AddSubgroup.map ↑f, invFun := AddSubgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafAddCommGroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (A : Type u)
  [inst_9 : TopologicalSpace A] [inst_10 : ChartedSpace H A] [inst_11 : AddCommGroup A]
  [inst_12 : LieAddGroup I (↑⊤) A],
  smoothSheafAddCommGroup IM I M A = { obj := smoothPresheafAddCommGroup IM I M A, property := ⋯ }
-- Mathlib.NumberTheory.Chebyshev
/-- Explicit upper bound on `ψ`.  -/
Chebyshev.psi_le : ∀ {x : ℝ}, 1 ≤ x → Chebyshev.psi x ≤ Real.log 4 * x + 2 * √x * Real.log x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        (m₁.diff! m₂).getKey? k = if Std.DTreeMap.Internal.Impl.contains k m₂ = true then none else m₁.getKey? k
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.mk.sizeOf_spec : ∀ {m : Type w → Type w'} {α : Type w} [inst : (a : Type w) → SizeOf (m a)] [inst_1 : SizeOf α] (Property : α → Prop)
  (operation : m (Subtype Property)), sizeOf { Property := Property, operation := operation } = 1 + sizeOf operation
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectedSystem.natLERec.directedSystem : ∀ {L : FirstOrder.Language} {G' : ℕ → Type w} [inst : (i : ℕ) → L.Structure (G' i)]
  (f' : (n : ℕ) → L.Embedding (G' n) (G' (n + 1))),
  DirectedSystem G' fun i j h => ⇑(FirstOrder.Language.DirectedSystem.natLERec f' i j h)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.writes.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Fintype Γ] (a : Turing.Dir) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.writes (Turing.TM1.Stmt.move a q) = Turing.TM1to1.writes q
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {δ : Type u_4}
  {mδ : MeasurableSpace δ} (γ : Type u_5) [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) (f : β → δ),
  (ProbabilityTheory.Kernel.prodMkLeft γ κ).map f = ProbabilityTheory.Kernel.prodMkLeft γ (κ.map f)
-- Mathlib.Order.RelIso.Basic
/-- Elements are related iff they are related after apply a `RelIso`  -/
RelIso.map_rel_iff' : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (self : r ≃r s) {a b : α},
  s (self.toEquiv a) (self.toEquiv b) ↔ r a b
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.WF.tail? : ∀ {α : Type u_1} {s : Batteries.PairingHeapImp.Heap α} {le : α → α → Bool} {tl : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.WF le s →
    Batteries.PairingHeapImp.Heap.tail? le s = some tl → Batteries.PairingHeapImp.Heap.WF le tl
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioi_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : Fintype β] [inst_4 : LocallyFiniteOrderTop β] (b : β),
  Finset.Ioi (Sum.inrₗ b) = Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Ioi b)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.stronglyMeasurable : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E} [OpensMeasurableSpace E]
  (f : ContDiffMapSupportedIn E F n K), MeasureTheory.StronglyMeasurable ⇑f
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.mem_cycles₁_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x : G →₀ ↑A),
  x ∈ groupHomology.cycles₁ A ↔ (x.sum fun g a => (A.ρ g⁻¹) a) = x.sum fun x a => a
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRcoSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRcoSlice._auto_1) →
      Std.Rco.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RcoSlice α β)
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.continuous_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y}, IsOpenQuotientMap f → ∀ {g : Y → Z}, Continuous (g ∘ f) ↔ Continuous g
-- Mathlib.Order.Sublattice
Sublattice.mem_pi : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] {s : Set κ} {L : (i : κ) → Sublattice (π i)}
  {x : (i : κ) → π i}, x ∈ Sublattice.pi s L ↔ ∀ i ∈ s, x i ∈ L i
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_filter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool},
  (Std.HashSet.filter f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = false
-- Mathlib.Analysis.LConvolution
/-- The convolution of measurable functions is measurable.  -/
MeasureTheory.measurable_lconvolution : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Add G] [inst_1 : Neg G] [MeasurableAdd₂ G] [MeasurableNeg G]
  {f g : G → ENNReal} (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ],
  Measurable f → Measurable g → Measurable (MeasureTheory.lconvolution f g μ)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forIn_eq_forIn : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m']
  [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn f init m = forIn m init fun a b => f a.fst a.snd b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertMany_list_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)},
  Std.ExtDHashMap.Const.insertMany m l = List.foldl (fun acc p => acc.insert p.1 p.2) m l
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two vector spaces are isomorphic if they have the same dimension.  -/
LinearEquiv.ofLiftRankEq : {R : Type u} →
  (M : Type v) →
    (M' : Type v') →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [Module.Free R M] →
              [inst_4 : AddCommMonoid M'] →
                [inst_5 : Module R M'] →
                  [Module.Free R M'] →
                    [StrongRankCondition R] →
                      Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M') → M ≃ₗ[R] M'
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.right_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Monad C) (X : C),
  CategoryTheory.CategoryStruct.comp (self.map (self.η.app X)) (self.μ.app X) =
    CategoryTheory.CategoryStruct.id (self.obj ((CategoryTheory.Functor.id C).obj X))
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.ext_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  {q₁ q₂ : QuaternionAlgebra.Basis A c₁ c₂ c₃}, q₁ = q₂ ↔ q₁.i = q₂.i ∧ q₁.j = q₂.j
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toExtension_algebra₁ : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), P.toExtension.algebra₁ = AddMonoidAlgebra.algebra
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- TODO: change proof to `rfl` when fixing https://github.com/leanprover-community/mathlib4/issues/18110.  -/
Algebra.toSubmodule_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Subalgebra.toSubmodule ⊥ = 1
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mapₗ_apply : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : Semiring R]
  [inst_1 : Semiring S] {σ : R →+* S} [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid B] [inst_4 : Module R A]
  [inst_5 : Module S B] (f : A →ₛₗ[σ] B) (M : CStarMatrix m n A), (CStarMatrix.mapₗ f) M = M.map ⇑f
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.eqvGen_step_iff_join_red : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  Relation.EqvGen FreeAddGroup.Red.Step L₁ L₂ ↔ Relation.Join FreeAddGroup.Red L₁ L₂
-- Mathlib.Analysis.Calculus.VectorField
/-- We have `[0, W] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable. Version within a set.  -/
VectorField.lieBracketWithin_zero_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {W : E → E} {s : Set E}, VectorField.lieBracketWithin 𝕜 0 W s = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Mathlib.Topology.EMetricSpace.Basic
/-- In an (e)metric space, every nontrivial type has a nontrivial topology.  -/
EMetric.instNontrivialTopologyOfNontrivial : ∀ {α : Type u_2} [inst : EMetricSpace α] [Nontrivial α], NontrivialTopology α
-- Mathlib.Algebra.Order.GroupWithZero.Defs
lt_mul_of_lt_mul_of_nonneg_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α],
  a < b * c → c ≤ d → 0 ≤ b → a < b * d
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (t.insertMany l).get? k = t.get? k
-- Init.Data.List.MinMaxIdx
/-- Returns the index of an element of the non-empty list `xs` that minimizes `f`.
If `x`, `y` are such that `f x = f y`, it returns the index of whichever comes first
in the list.

The correctness of this function assumes `β` to be linearly pre-ordered.
 -/
List.minIdxOn : {β : Type u_1} → {α : Type u_2} → [inst : LE β] → [DecidableLE β] → (α → β) → (xs : List α) → xs ≠ [] → ℕ
-- Mathlib.Algebra.CharP.MixedCharZero
MixedCharZero.charP_quotient : ∀ {R : Type u_1} {inst : CommRing R} {p : ℕ} [self : MixedCharZero R p], ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
-- Mathlib.RingTheory.Congruence.Hom
RingCon.congrₐ_symm : ∀ {M : Type u_1} {N : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring N] [inst_4 : Algebra R N] {c : RingCon M} {d : RingCon N} (e : M ≃ₐ[R] N) (h : c = d.comap e),
  (RingCon.congrₐ R e h).symm = RingCon.congrₐ R e.symm ⋯
-- Lean.Elab.DeclModifiers
Lean.Elab.Visibility.regular.sizeOf_spec : sizeOf Lean.Elab.Visibility.regular = 1
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_eq_zero_of_num : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A} (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x),
  f.num = 0 → HomogeneousLocalization.mk f = 0
-- Mathlib.Topology.Order.MonotoneConvergence
/-- **Alias** of `tendsto_atTop_of_antitone`. -/
tendsto_of_antitone : ∀ {ι : Type u_3} {α : Type u_4} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α},
  Antitone f → Filter.Tendsto f Filter.atTop Filter.atBot ∨ ∃ l, Filter.Tendsto f Filter.atTop (nhds l)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.isUnit_addU_of_Y_ne : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3 → IsUnit (WeierstrassCurve.Jacobian.addU P Q)
-- Mathlib.Data.ZMod.Basic
ZMod.val_one' : ZMod.val 1 = 1
-- Mathlib.Order.Hom.Lex
Prod.Lex.sumLexProdLexDistrib_apply : ∀ (α : Type u_4) (β : Type u_5) (γ : Type u_6) [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (a : Lex ((α ⊕ₗ β) × γ)),
  (Prod.Lex.sumLexProdLexDistrib α β γ) a =
    toLex (Sum.map (⇑toLex) (⇑toLex) ((Equiv.sumProdDistrib α β γ) (Prod.map (⇑ofLex) id (ofLex a))))
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_sq : ∀ (x : ℝ), Real.sin x ^ 2 = 1 - Real.cos x ^ 2
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote.match_1.eq_6 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (k : ℤ) (a : Lean.Grind.Linarith.Expr)
  (h_1 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_2 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_3 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b))
  (h_5 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (h_6 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_7 : (a : Lean.Grind.Linarith.Expr) → motive a.neg),
  (match Lean.Grind.Linarith.Expr.intMul k a with
    | Lean.Grind.Linarith.Expr.zero => h_1 ()
    | Lean.Grind.Linarith.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_5 k a
    | Lean.Grind.Linarith.Expr.intMul k a => h_6 k a
    | a.neg => h_7 a) =
    h_6 k a
-- Mathlib.CategoryTheory.Products.Basic
/-- Construct a morphism in a product category by giving its constituent components.
This constructor should be preferred over `Prod.mk`, because Lean infers better the
source and target of the resulting morphism.  -/
CategoryTheory.Prod.«term_×ₘ_» : Lean.TrailingParserDescr
-- Mathlib.ModelTheory.Definability
/-- Constant functions are `TermDefinable₁`, assuming the constant value is a language constant.  -/
Set.TermDefinable₁.const : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] (C : (L.withConstants ↑A).Constants),
  Set.TermDefinable₁ L (Function.const M ↑C)
-- Mathlib.LinearAlgebra.TensorProduct.Pi
TensorProduct.piRight_symm_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_7 : (i : ι) → AddCommMonoid (M i)] [inst_8 : (i : ι) → Module R (M i)] [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (x : N) (m : (i : ι) → M i),
  ((TensorProduct.piRight R S N M).symm fun i => x ⊗ₜ[R] m i) = x ⊗ₜ[R] m
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioo_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioo (n • b) ((n + 1) • b))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constInsertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {l : List (α × β)},
      (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t₁ l ⋯)).Equiv
        ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t₂ l ⋯)
-- Mathlib.Data.Complex.Basic
Complex.normSq_sub : ∀ (z w : ℂ), Complex.normSq (z - w) = Complex.normSq z + Complex.normSq w - 2 * (z * (starRingEnd ℂ) w).re
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.mk : {α : Type} → Std.Mutex (Std.CloseableChannel.Unbounded.State✝ α) → Std.CloseableChannel.Unbounded✝ α
-- Mathlib.Algebra.Group.MinimalAxioms
AddGroup.ofLeftAxioms.eq_1 : ∀ {G : Type u} [inst : Add G] [inst_1 : Neg G] [inst_2 : Zero G] (assoc : ∀ (a b c : G), a + b + c = a + (b + c))
  (one_mul : ∀ (a : G), 0 + a = a) (inv_mul_cancel : ∀ (a : G), -a + a = 0),
  AddGroup.ofLeftAxioms assoc one_mul inv_mul_cancel =
    { toAdd := inst, add_assoc := assoc, toZero := inst_2, zero_add := one_mul, add_zero := ⋯, nsmul := nsmulRecAuto,
      nsmul_zero := ⋯, nsmul_succ := ⋯, toNeg := inst_1, sub := SubNegMonoid.sub', zsmul := zsmulRec,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := inv_mul_cancel }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul'`.  -/
Left.one_lt_mul' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, 1 < a → 1 < b → 1 < a * b
-- Mathlib.Data.Sum.Interval
Sum.Lex.Icc_inl_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a₁ a₂ : α),
  Finset.Icc (Sum.inlₗ a₁) (Sum.inlₗ a₂) =
    Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Icc a₁ a₂)
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.integralNormalization 0 = 0
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjointDomainMkCLMExtend_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →ₗ.[𝕜] F},
  Dense ↑T.domain → ∀ (y : ↥T.adjointDomain) (x : ↥T.domain), (T.adjointDomainMkCLMExtend y) ↑x = inner 𝕜 (↑y) (↑T x)
-- Mathlib.Algebra.GroupWithZero.Basic
/-- A variant of `pow_eq_zero_iff` assuming `M₀` is not trivial.  -/
pow_eq_zero_iff' : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] [Nontrivial M₀], a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_filter!_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} {k : α},
  t.WF →
    (Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter! f t) = true ↔
      ∃ (h' : Std.DTreeMap.Internal.Impl.contains k t = true),
        f (t.getKey k h') (Std.DTreeMap.Internal.Impl.Const.get t k h') = true)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.uniq_terminal : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  (self : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) (j : J)
  (hj : self.IsTerminal j), j = self.top
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_mem_Ioo_iff_sign_pos : ∀ {θ : Real.Angle}, θ.toReal ∈ Set.Ioo 0 Real.pi ↔ θ.sign = 1
-- Lean.Class
_private.Lean.Class.0.Lean.computeOutLevelParams.go : Array ℕ → Lean.Expr → ℕ → Lean.CollectLevelParams.State → Lean.CollectLevelParams.State
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
/-- Let `m` be a sub-σ-algebra of `m0`, `f` an `m0`-measurable function and `g` an `m`-measurable
function, such that their integrals coincide on `m`-measurable sets with finite measure.
Then `∫⁻ x in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ x in s, ‖f x‖ₑ ∂μ` on all `m`-measurable sets with finite
measure.  -/
MeasureTheory.lintegral_enorm_le_of_forall_fin_meas_integral_eq : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  m ≤ m0 →
    ∀ {f g : α → ℝ},
      MeasureTheory.StronglyMeasurable f →
        MeasureTheory.IntegrableOn f s μ →
          MeasureTheory.StronglyMeasurable g →
            MeasureTheory.IntegrableOn g s μ →
              (∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ) →
                MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ
-- Lean.Parser.Basic
Lean.Parser.checkStackTop : (Lean.Syntax → Bool) → String → Lean.Parser.Parser
-- Mathlib.Data.Sym.Basic
Sym.append_comm : ∀ {α : Type u_1} {n' : ℕ} (s s' : Sym α n'), s.append s' = (Sym.cast ⋯) (s'.append s)
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.image_coe_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithBot.some '' Set.Ico b a = Set.Ico ↑b ↑a
-- Aesop.Tree.Data
Aesop.RappId.succ : Aesop.RappId → Aesop.RappId