mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
/-- The natural isomorphism `NΓ'` satisfies the compatibility that is needed
for the construction of our counit isomorphism `η`.  -/
CategoryTheory.Idempotents.DoldKan.hη : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C],
  AlgebraicTopology.DoldKan.Compatibility.τ₀ =
    AlgebraicTopology.DoldKan.Compatibility.τ₁ CategoryTheory.Idempotents.DoldKan.isoN₁
      CategoryTheory.Idempotents.DoldKan.isoΓ₀ AlgebraicTopology.DoldKan.N₁Γ₀
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'_two : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 2 = 1
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar.congr_simp : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [inst_5 : IsAbelianGalois ℚ K],
  IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R =
    IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R
-- Mathlib.CategoryTheory.Sites.Point.Over
CategoryTheory.GrothendieckTopology.instHasEnoughPointsOverOverOfWEqualsLocallyBijectiveFunOfHasSheafifyType : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [CategoryTheory.LocallySmall.{w, v, u} C] [J.HasEnoughPoints] [J.WEqualsLocallyBijective (Type w)]
  [CategoryTheory.HasSheafify J (Type w)] (X : C) [CategoryTheory.HasSheafify (J.over X) (Type w)],
  (J.over X).HasEnoughPoints
-- Mathlib.Analysis.Complex.Exponential
/-- The Cauchy sequence consisting of partial sums of the Taylor series of
the complex exponential function  -/
Complex.exp' : ℂ → CauSeq ℂ fun x => ‖x‖
-- Mathlib.LinearAlgebra.Charpoly.Basic
/-- Any endomorphism polynomial `p` is equivalent under evaluation to `p %ₘ f.charpoly`; that is,
`p` is equivalent to a polynomial with degree less than the dimension of the module.  -/
LinearMap.aeval_eq_aeval_mod_charpoly : ∀ {R : Type u} {M : Type v} [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) (p : Polynomial R),
  (Polynomial.aeval f) p = (Polynomial.aeval f) (p %ₘ f.charpoly)
-- Mathlib.Computability.Language
Symbol.terminal.sizeOf_spec : ∀ {T : Type u_4} {N : Type u_5} [inst : SizeOf T] [inst_1 : SizeOf N] (t : T), sizeOf (Symbol.terminal t) = 1 + sizeOf t
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapMapIso_counitIso : ∀ {X Y : TopCat} (H : X ≅ Y),
  (TopologicalSpace.Opens.mapMapIso H).counitIso =
    CategoryTheory.NatIso.ofComponents (fun U => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.LinearAlgebra.DFinsupp
LinearMap.coe_dfinsuppSum : ∀ {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {γ : ι → Type u_12} [inst_6 : DecidableEq ι] [inst_7 : (i : ι) → Zero (γ i)]
  [inst_8 : (i : ι) → (x : γ i) → Decidable (x ≠ 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂),
  ⇑(t.sum g) = ⇑(t.sum fun i d => g i d)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_diff_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ((t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂)
-- Init.Data.Range.Polymorphic.PRange
/-- This type class allows taking the intersection of an open range with a
left-closed right-open range, resulting in another left-closed right-open range.
 -/
Std.Roo.HasRcoIntersection : Type w → Type w
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (refs : Vector Std.Sat.AIG.Fanin w) (hrefs : ∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse aig { refs := refs, hrefs := hrefs } =
    { aig := aig, vec := { refs := refs.reverse, hrefs := ⋯ } }
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.preconnected_iff : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Preconnected ↔ H.coe.Preconnected
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Polynomial.residueFieldMapCAlgEquiv.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime] (J : Ideal (Polynomial R)) [inst_2 : J.IsPrime]
  [inst_3 : J.LiesOver I] [inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
  [inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J] (hJ : J = Ideal.map Polynomial.C I),
  Polynomial.residueFieldMapCAlgEquiv I J hJ =
    AlgEquiv.ofAlgHom
      {
        toRingHom :=
          Ideal.ResidueField.lift J
            ((algebraMap (Polynomial I.ResidueField) (RatFunc I.ResidueField)).comp
              (Polynomial.mapRingHom (algebraMap R I.ResidueField)))
            ⋯ ⋯,
        commutes' := ⋯ }
      (RatFunc.liftAlgHom (Polynomial.aeval ((algebraMap (Polynomial R) J.ResidueField) Polynomial.X)) ⋯) ⋯ ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alterₘ.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] (k k_1 : α),
  k = k_1 →
    ∀ (f f_1 : Option β → Option β),
      f = f_1 →
        ∀ (t t_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t : t = t_1) (h : t.Balanced),
          Std.DTreeMap.Internal.Impl.Const.alterₘ k f t h = Std.DTreeMap.Internal.Impl.Const.alterₘ k_1 f_1 t_1 ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.isStableUnderCoproductsOfShape_trivialCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] (J : Type w),
  (HomotopicalAlgebra.trivialCofibrations C).IsStableUnderCoproductsOfShape J
-- Mathlib.RingTheory.Perfectoid.BDeRham
/-- The Fontaine's θ map inverting `p`. Note that if `p = 0` in `R`, then this is the zero map.
 -/
fontaineThetaInvertP : (R : Type u) →
  [inst : CommRing R] →
    (p : ℕ) →
      [inst_1 : Fact (Nat.Prime p)] →
        [inst_2 : Fact ¬IsUnit ↑p] →
          [IsAdicComplete (Ideal.span {↑p}) R] → Localization.Away ↑p →+* Localization.Away ↑p
-- Mathlib.Algebra.Group.Action.End
AddAction.toPermHom_apply_symm_apply : ∀ (G : Type u_1) (α : Type u_5) [inst : AddGroup G] [inst_1 : AddAction G α] (a : G) (x : α),
  (Equiv.symm ((AddAction.toPermHom G α) a)) x = (Multiplicative.ofAdd a)⁻¹ • x
-- Init.Notation
/-- `with_annotate_term stx e` annotates the lexical range of `stx : Syntax` with term info for `e`.  -/
Lean.withAnnotateTerm : Lean.ParserDescr
-- Std.Tactic.BVDecide.LRAT.Internal.PosFin
Std.Tactic.BVDecide.LRAT.Internal.PosFin : ℕ → Type
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get!.eq_def : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] (a : α)
  (x : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.get! a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil =>
      panicWithPosWithDecl "Std.Data.DHashMap.Internal.AssocList.Basic" "Std.DHashMap.Internal.AssocList.get!" 163 11
        "key is not present in hash table"
    | Std.DHashMap.Internal.AssocList.cons k v es => bif k == a then v else Std.DHashMap.Internal.AssocList.get! a es
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.minNatAbs_eq_zero_iff : ∀ {xs : List ℤ}, Lean.Elab.Tactic.Omega.List.minNatAbs xs = 0 ↔ ∀ y ∈ xs, y = 0
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.map_comp_map : ∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {W₁ : Type u_6} {W₂ : Type u_7}
  {W₃ : Type u_8} [inst_3 : SeminormedAddCommGroup W₁] [inst_4 : SeminormedAddCommGroup W₂]
  [inst_5 : SeminormedAddCommGroup W₃] {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂}
  {f₃ g₃ : NormedAddGroupHom V₃ W₃} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂}
  {φ' : NormedAddGroupHom V₂ V₃} {ψ' : NormedAddGroupHom W₂ W₃} (hf : ψ.comp f₁ = f₂.comp φ)
  (hg : ψ.comp g₁ = g₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') (hg' : ψ'.comp g₂ = g₃.comp φ'),
  (NormedAddGroupHom.Equalizer.map φ' ψ' hf' hg').comp (NormedAddGroupHom.Equalizer.map φ ψ hf hg) =
    NormedAddGroupHom.Equalizer.map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Transfer the arguments to a map along an equivalence between argument indices.

This is the alternating version of `MultilinearMap.domDomCongr`.  -/
AlternatingMap.domDomCongr : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] → {ι : Type u_7} → {ι' : Type u_8} → ι ≃ ι' → M [⋀^ι]→ₗ[R] N → M [⋀^ι']→ₗ[R] N
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_map_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLEGT n).map φ).hom₁ = (t.truncLE n).map φ
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.mk.inj : ∀ {α : Type u} {β : Type v} {inner inner_1 : Std.DHashMap.Raw α fun x => β},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Topology.Separation.Regular
Homeomorph.t3Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T3Space X] (h : X ≃ₜ Y),
  T3Space Y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km : α} {hc : Std.Internal.List.containsKey km l = true},
      (Std.Internal.List.minKey? l).get ⋯ = km → Std.Internal.List.getKey km l hc = km
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.elabBinderViews : {α : Type} →
  Array Lean.Elab.Term.BinderView →
    Array (Lean.Syntax × Lean.Expr) → (Array (Lean.Syntax × Lean.Expr) → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Analysis.Convex.GaugeRescale
gaugeRescale_gaugeRescale : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [T1Space E]
  {s t u : Set E},
  Absorbent ℝ t → Bornology.IsVonNBounded ℝ t → ∀ (x : E), gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_X : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.I₀ × 𝒰Y.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).X ij =
    CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰X.f ij.1) f)
      (CategoryTheory.CategoryStruct.comp (𝒰Y.f ij.2) g)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_eq_single : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {f : α →₀ M} (a : α)
  {g : α → M → N}, (∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 0) → (f a = 0 → g a 0 = 0) → f.sum g = g a (f a)
-- Mathlib.Order.Irreducible
not_infIrred_top : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderTop α], ¬InfIrred ⊤
-- Init.Data.List.Sublist
List.suffix_iff_exists_eq_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ ↔ ∃ l₃, l₂ = l₃ ++ l₁
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → UpperSet α),
  ↑(⨅ i, ⨅ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)
-- Batteries.Data.BitVec.Lemmas
BitVec.ofFnBE.eq_1 : ∀ {n : ℕ} (f : Fin n → Bool), BitVec.ofFnBE f = BitVec.ofFnLE fun i => f i.rev
-- Mathlib.FieldTheory.Cardinality
_private.Mathlib.FieldTheory.Cardinality.0.«term‖_‖» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.homCategory.ext_iff : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ}, m = n ↔ ∀ (a : B), m.as.app a = n.as.app a
-- Init.Data.Vector.Lemmas
Vector.mem_iff_getElem? : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, a ∈ xs ↔ ∃ i, xs[i]? = some a
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.mem_toList_iff_isPlausibleIndirectOutput : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Std.LawfulDeterministicIterator α Id]
  {it : Std.Iter β} {out : β}, out ∈ it.toList ↔ it.IsPlausibleIndirectOutput out
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.toIntCast : {R : Type u} → [self : AddGroupWithOne R] → IntCast R
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preLeft.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T),
  CategoryTheory.Comma.preLeft F L R =
    { obj := fun X => { left := F.obj X.left, right := X.right, hom := X.hom },
      map := fun {X Y} f => { left := F.map f.left, right := f.right, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceHoverParams : Lean.Lsp.FileSource Lean.Lsp.HoverParams
-- Mathlib.Topology.Order.LeftRightLim
Antitone.tendsto_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f →
    ∀ [inst_4 : TopologicalSpace α] [OrderTopology α] (x : α),
      Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLim f x))
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (Std.TreeMap.Raw.ofList l cmp).getD k fallback = fallback
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_filterMap : ∀ {α β γ δ : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : Std.Iter β},
  Std.Iter.fold g init (Std.Iter.filterMap f it) =
    Std.Iter.fold
      (fun d b =>
        match f b with
        | some c => g d c
        | x => d)
      init it
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.trace_eq_sum_eigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.trace = ∑ i, ↑(hA.eigenvalues i)
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.toMeasure_ofFintype_apply : ∀ {α : Type u_1} [inst : Fintype α] {f : α → ENNReal} (h : ∑ a, f a = 1) (s : Set α) [inst_1 : MeasurableSpace α],
  MeasurableSet s → (PMF.ofFintype f h).toMeasure s = ∑' (x : α), s.indicator f x
-- Mathlib.Data.Nat.MaxPowDiv
/-- Auxiliary definition for `Nat.maxPowDvdDiv`.  -/
Nat.maxPowDvdDiv.go : (n p : ℕ) → 1 < p ∧ n ≠ 0 → ℕ × ℕ
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.applyDerivingHandlers : Array Lean.Elab.Command.InductiveView → Lean.Elab.Command.CommandElabM Unit
-- Lean.Expr
Lean.ExprStructEq.mk : Lean.Expr → Lean.ExprStructEq
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality**, a version for nonnegative real numbers.  -/
Real.young_inequality_of_nonneg : ∀ {a b p q : ℝ}, 0 ≤ a → 0 ≤ b → p.HolderConjugate q → a * b ≤ a ^ p / p + b ^ q / q
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal.eq_1 : ∀ (c : ℝ), Tactic.ComputeAsymptotics.MultiseriesExpansion.ofReal c = c
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain_comapDomain : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] {f : M → N} {x : AddMonoidAlgebra R N},
  ↑x.coeff.support ⊆ Set.range f →
    ∀ (hf : Function.Injective f), AddMonoidAlgebra.mapDomain f (AddMonoidAlgebra.comapDomain f hf x) = x
-- Mathlib.Algebra.Group.Submonoid.Finite
/-- For finite index types, the `Submonoid.pi` is generated by the embeddings of the
additive monoids.  -/
AddSubmonoid.pi_le_iff : ∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → AddZeroClass (f i)] [Finite η] [inst_2 : DecidableEq η]
  {H : (i : η) → AddSubmonoid (f i)} {J : AddSubmonoid ((i : η) → f i)},
  AddSubmonoid.pi Set.univ H ≤ J ↔ ∀ (i : η), AddSubmonoid.map (AddMonoidHom.single f i) (H i) ≤ J
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopicRel.refl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set X} (f : C(X, Y)),
  f.HomotopicRel f S
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.completeLattice : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : StarRing A] → [inst_5 : StarModule R A] → CompleteLattice (StarSubalgebra R A)
-- Mathlib.Control.Fix
Part.Fix.approx.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)), Part.Fix.approx f 0 = ⊥
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β},
  s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Subfield.extendScalars_inf : ∀ {L : Type u_2} [inst : Field L] {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E'),
  Subfield.extendScalars h ⊓ Subfield.extendScalars h' = Subfield.extendScalars ⋯
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.map.congr_simp : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f f_1 : 𝒜 →+*ᵍ ℬ) (e_f : f = f_1)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)),
  AlgebraicGeometry.Proj.map f hf = AlgebraicGeometry.Proj.map f_1 ⋯
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.hom_ext_iff : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} {f g : X ⟶ Y},
  f = g ↔
    CategoryTheory.Arrow.Hom.left f = CategoryTheory.Arrow.Hom.left g ∧
      CategoryTheory.Arrow.Hom.right f = CategoryTheory.Arrow.Hom.right g
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSolverTerms : Inhabited Lean.Meta.Grind.SolverTerms
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.getSomeSyntheticMVarsRef : Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.prod_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α), μ.prod 0 = 0
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp F U c).hom.hom =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))).obj
          c).pt
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.ofBoxProdLeft.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [inst : DecidableEq β]
  [inst_1 : DecidableRel G.Adj] {x y : α × β} (v : α × β) (h : (G □ H).Adj x v) (w : (G □ H).Walk v y),
  (SimpleGraph.Walk.cons h w).ofBoxProdLeft =
    Or.by_cases h (fun hG => SimpleGraph.Walk.cons ⋯ w.ofBoxProdLeft) fun hH => ⋯ ▸ w.ofBoxProdLeft
-- Mathlib.Logic.Basic
forall_true_iff' : ∀ {α : Sort u_1} {p : α → Prop}, (∀ (a : α), p a ↔ True) → ((∀ (a : α), p a) ↔ True)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.Nonempty.zero_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] {t : Set β},
  t.Nonempty → 0 • t = 0
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedConfig : Inhabited Lean.Meta.Sym.Config
-- Lean.Meta.Basic
/-- Returns `some value` if the given free let-variable has a visible local definition in the current local context
(using `Lean.LocalDecl.value?`), and `none` otherwise.

Setting `allowNondep := true` allows access of the normally hidden value of a nondependent let declaration.
 -/
Lean.FVarId.getValue? : Lean.FVarId → optParam Bool false → Lean.MetaM (Option Lean.Expr)
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then their
inseparable degrees, as natural numbers, satisfy the tower law: $[E:F]_i [K:E]_i = [K:F]_i$.  -/
Field.finInsepDegree_mul_finInsepDegree_of_isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E],
  Field.finInsepDegree F E * Field.finInsepDegree E K = Field.finInsepDegree F K
-- Std.Data.HashMap.Basic
/-- Computes the union of the given hash maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashMap.union : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → Std.HashMap α β → Std.HashMap α β
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.comp_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [mα : MeasurableSpace α] {x : MeasurableSpace β}
  [inst : TopologicalSpace γ] {f : β → γ},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun z => f z.2
-- Init.Data.UInt.Lemmas
UInt32.mul_sub : ∀ {a b c : UInt32}, a * (b - c) = a * b - a * c
-- Mathlib.Algebra.Module.Submodule.Lattice
/-- The bottom submodule is linearly equivalent to punit as an `R`-module.  -/
Submodule.botEquivPUnit : {R : Type u_1} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → ↥⊥ ≃ₗ[R] PUnit.{v + 1}