mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  LowerSet.instCommMonoid =
    { toSemigroup := LowerSet.commSemigroup.toSemigroup, toOne := LowerSet.instOne, one_mul := ⋯, mul_one := ⋯,
      npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- Given `P : ObjectProperty C` with `C` a pretriangulated category, this is the class
of morphisms whose cone satisfies `P`. (The name `trW` contains the prefix `tr`
for "triangulated", and `W` is a letter that is often used to refer to classes of
morphisms with respect to which we may consider the localized category.)  -/
CategoryTheory.ObjectProperty.trW : {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] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_lt_iff_lt_embedding : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R} {g : (MonoidWithZeroHom.ofClass v).ValueGroup₀},
  v.restrict x < g ↔ v x < MonoidWithZeroHom.ValueGroup₀.embedding g
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instMul : (K : Type u) →
  [inst : CommRing K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → Mul (PerfectClosure K p)
-- Mathlib.Algebra.DirectSum.Basic
/-- The natural equivalence between `⨁ _ : ι, M` and `M` when `Unique ι`.  -/
DirectSum.id : (M : Type v) →
  (ι : optParam (Type u_1) PUnit.{u_1 + 1}) → [inst : AddCommMonoid M] → [Unique ι] → (DirectSum ι fun x => M) ≃+ M
-- Mathlib.Order.KrullDimension
Order.krullDim_eq_bot : ∀ {α : Type u_1} [inst : Preorder α] [IsEmpty α], Order.krullDim α = ⊥
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.StronglyConnectedComponent.instInhabited : {V : Type u_2} → [inst : Quiver V] → [Inhabited V] → Inhabited (Quiver.StronglyConnectedComponent V)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffOn_pi' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  (∀ (i : ι), ContDiffOn 𝕜 n (fun x => Φ x i) s) → ContDiffOn 𝕜 n Φ s
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `continuous_const_mul`. -/
continuous_mul_left : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] (m : M),
  Continuous fun x => m * x
-- Std.Time.Time.PlainTime
/-- Creates a `PlainTime` value from a total number of minutes.
 -/
Std.Time.PlainTime.ofMinutes : Std.Time.Minute.Offset → Std.Time.PlainTime
-- Mathlib.Algebra.Order.Kleene
/-- Pullback a `KleeneAlgebra` instance along an injective function.  -/
Function.Injective.kleeneAlgebra : {α : Type u_1} →
  {β : Type u_2} →
    [inst : KleeneAlgebra α] →
      [inst_1 : LE β] →
        [inst_2 : LT β] →
          [inst_3 : Zero β] →
            [inst_4 : One β] →
              [inst_5 : Add β] →
                [inst_6 : Mul β] →
                  [inst_7 : Pow β ℕ] →
                    [inst_8 : SMul ℕ β] →
                      [inst_9 : NatCast β] →
                        [inst_10 : Max β] →
                          [inst_11 : Bot β] →
                            [inst_12 : KStar β] →
                              (f : β → α) →
                                Function.Injective f →
                                  (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) →
                                    (∀ {x y : β}, f x < f y ↔ x < y) →
                                      f 0 = 0 →
                                        f 1 = 1 →
                                          (∀ (x y : β), f (x + y) = f x + f y) →
                                            (∀ (x y : β), f (x * y) = f x * f y) →
                                              (∀ (n : ℕ) (x : β), f (n • x) = n • f x) →
                                                (∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                  (∀ (n : ℕ), f ↑n = ↑n) →
                                                    (∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) →
                                                      f ⊥ = ⊥ →
                                                        (∀ (a : β), f (KStar.kstar a) = KStar.kstar (f a)) →
                                                          KleeneAlgebra β
-- Std.Net.Addr
Std.Net.IPv4Addr.instToString : ToString Std.Net.IPv4Addr
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.RiemannianMetric.mk.injEq : ∀ {B : Type u_4} {E : B → Type u_6} [inst : (b : B) → TopologicalSpace (E b)] [inst_1 : (b : B) → AddCommGroup (E b)]
  [inst_2 : (b : B) → Module ℝ (E b)] (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ)
  (symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v)
  (pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v)
  (continuousAt : ∀ (b : B), ContinuousAt (fun v => ((inner b) v) v) 0)
  (isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1})
  (inner_1 : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) (symm_1 : ∀ (b : B) (v w : E b), ((inner_1 b) v) w = ((inner_1 b) w) v)
  (pos_1 : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner_1 b) v) v)
  (continuousAt_1 : ∀ (b : B), ContinuousAt (fun v => ((inner_1 b) v) v) 0)
  (isVonNBounded_1 : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner_1 b) v) v < 1}),
  ({ inner := inner, symm := symm, pos := pos, continuousAt := continuousAt, isVonNBounded := isVonNBounded } =
      { inner := inner_1, symm := symm_1, pos := pos_1, continuousAt := continuousAt_1,
        isVonNBounded := isVonNBounded_1 }) =
    (inner = inner_1)
-- Mathlib.Algebra.Order.Floor.Extended
/-- `⌊r⌋ₑ` is the greatest extended natural `n` such that `n ≤ r`.  -/
ENat.floor : ENNReal → ℕ∞
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
/-- The Geck construction yields a basis of the Lie algebra it constructs.  -/
RootPairing.GeckConstruction.basis : {ι : Type u_1} →
  {K : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Fintype ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : Field K] →
              [inst_3 : CharZero K] →
                [inst_4 : AddCommGroup M] →
                  [inst_5 : Module K M] →
                    [inst_6 : AddCommGroup N] →
                      [inst_7 : Module K N] →
                        {P : RootPairing ι K M N} →
                          [P.IsReduced] →
                            [inst_9 : P.IsCrystallographic] →
                              [P.IsIrreducible] →
                                [P.IsRootSystem] →
                                  (b : P.Base) →
                                    LieAlgebra.Basis (↥b.support) (RootPairing.GeckConstruction.cartanSubalgebra' b)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono_set : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f : X → E}
  {s t : Set X} [OrderClosedTopology E],
  MeasureTheory.IntegrableOn f t μ → 0 ≤ᵐ[μ.restrict t] f → s ≤ᵐ[μ] t → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in t, f x ∂μ
-- Init.Data.List.Monadic
List.forIn'.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α) (init : β)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)), as.forIn' init f = List.forIn'.loop as f as init ⋯
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (x : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteS ctx x =
    match x with
    | Lean.Grind.CommRing.Expr.num k => OfNat.ofNat k.natAbs
    | Lean.Grind.CommRing.Expr.natCast k => OfNat.ofNat k
    | Lean.Grind.CommRing.Expr.var v => Lean.Grind.CommRing.Var.denote ctx v
    | a.add b => Lean.Grind.CommRing.Expr.denoteS ctx a + Lean.Grind.CommRing.Expr.denoteS ctx b
    | a.mul b => Lean.Grind.CommRing.Expr.denoteS ctx a * Lean.Grind.CommRing.Expr.denoteS ctx b
    | a.pow k => Lean.Grind.CommRing.Expr.denoteS ctx a ^ k
    | a.sub b => 0
    | a.neg => 0
    | Lean.Grind.CommRing.Expr.intCast k => 0
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_mul_right_closedEBall : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x * a) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (b / a) r
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- An alternative version of `Subcomplex.mk`: Instead of requiring that `E` is closed it requires
that `E` is a CW-complex.  -/
Topology.RelCWComplex.Subcomplex.mk'' : {X : Type u_1} →
  [t : TopologicalSpace X] →
    [T2Space X] →
      (C : Set X) →
        {D : Set X} →
          [inst : Topology.RelCWComplex C D] →
            (E : Set X) →
              (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) →
                [Topology.RelCWComplex E D] →
                  D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E → Topology.RelCWComplex.Subcomplex C
-- Mathlib.Topology.Category.TopCat.ULift
TopCat.uliftFunctorObjHomeo_naturality_apply : ∀ {X Y : TopCat} (f : X ⟶ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (TopCat.uliftFunctor.map f)) (X.uliftFunctorObjHomeo x) =
    Y.uliftFunctorObjHomeo ((CategoryTheory.ConcreteCategory.hom f) x)
-- Init.Data.SInt.Lemmas
Int32.zero_sub : ∀ (a : Int32), 0 - a = -a
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.ιNormalizedChainComplex_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) {R : C} {n : ℕ},
  ∀ x ∈ X.degenerate n, X.ιNormalizedChainComplex x = 0
-- Init.GrindInstances.Ring.UInt
USize.instOfNat.eq_1 : ∀ {n : ℕ}, USize.instOfNat = { ofNat := USize.ofNat n }
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_4.eq_1 : ∀ (motive : Option Lean.Expr → Sort u_1) (r : Lean.Expr) (h_1 : (r : Lean.Expr) → motive (some r))
  (h_2 : (x : Option Lean.Expr) → motive x),
  (match some r with
    | some r => h_1 r
    | x => h_2 x) =
    h_1 r
-- Mathlib.Tactic.Linter.Style
/-- The `dollarSyntax` linter flags uses of `<|` that are achieved by typing `$`.
These are disallowed by the mathlib style guide, as using `<|` pairs better with `|>`.  -/
Mathlib.Linter.linter.style.dollarSyntax : Lean.Option Bool
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.homMk.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.RightLift f g} (η η_1 : s.lift ⟶ t.lift) (e_η : η = η_1)
  (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η f) t.counit = s.counit),
  CategoryTheory.Bicategory.RightLift.homMk η w = CategoryTheory.Bicategory.RightLift.homMk η_1 ⋯
-- Init.Data.BitVec.Lemmas
/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is nonneg.  -/
BitVec.toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg : ∀ {w : ℕ} {x y : BitVec w}, x.toInt ≤ 0 → 0 ≤ y.toInt → x.toInt / y.toInt ≤ 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfConeEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ},
  CategoryTheory.Limits.coconeLeftOpOfConeEquiv =
    {
      functor :=
        { obj := fun c => CategoryTheory.Limits.coconeLeftOpOfCone (Opposite.unop c),
          map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ },
      inverse :=
        { obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeLeftOp c),
          map := fun {X Y} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ },
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ),
      counitIso :=
        CategoryTheory.Iso.refl
          ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coneOfCoconeLeftOp c),
                map := fun {X Y} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
            { obj := fun c => CategoryTheory.Limits.coconeLeftOpOfCone (Opposite.unop c),
              map := fun {X Y} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }),
      functor_unitIso_comp := ⋯ }
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.subset_preimage : ∀ {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] {a : A} {f : S → R} [IsScalarTower S A A]
  [SMulCommClass S A A] [IsScalarTower R S A], QuasispectrumRestricts a f → quasispectrum S a ⊆ f ⁻¹' quasispectrum R a
-- Lean.Elab.Util
Lean.Elab.logException : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → [MonadLiftT IO m] → Lean.Exception → m Unit
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split'.eq_2 : ∀ (e : ONote) (n : ℕ+) (a : ONote),
  (e.oadd n a).split' =
    if e = 0 then (0, ↑n)
    else
      match a.split' with
      | (a', m) => ((e - 1).oadd n a', m)
-- Mathlib.Data.Multiset.UnionInter
Multiset.instLattice : {α : Type u_1} → [DecidableEq α] → Lattice (Multiset α)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} {f g : a ⟶ b} (a_1 : f ⟶ g)
  (x_1 : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda.obj x).map₂ a_1).toNatTrans.app x_1 =
    CategoryTheory.Bicategory.whiskerRight a_1.unop2 x_1
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.sumTransform.eq_1 : ∀ (p : ℝ) (g : ℝ → ℝ) (n₀ n : ℕ),
  AkraBazziRecurrence.sumTransform p g n₀ n = ↑n ^ p * ∑ u ∈ Finset.Ico n₀ n, g ↑u / ↑u ^ (p + 1)
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.counitNat_X : ∀ {A : Type u_1} [inst : CommSemiring A] (a : A), (MvPolynomial.counitNat A) (MvPolynomial.X a) = a
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.familyOfBFamily'.eq_1 : ∀ {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o)
  (f : (a : Ordinal.{u}) → a < o → α) (i : ι),
  Ordinal.familyOfBFamily' r ho f i = f ((Ordinal.typein r).toRelEmbedding i) ⋯
-- Mathlib.RingTheory.Unramified.Finite
Algebra.FormallyUnramified.sec.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  [inst_7 : Algebra.FormallyUnramified R S] [inst_8 : Algebra.EssFiniteType R S],
  Algebra.FormallyUnramified.sec R S M =
    {
      toAddHom :=
        (((TensorProduct.AlgebraTensorModule.mapBilinear R S S S S S M) LinearMap.id).flip
              (Algebra.FormallyUnramified.elem R S) ∘ₗ
            (Algebra.lsmul R R M).toLinearMap.flip).toAddHom,
      map_smul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)]
  {Z : C} (h : X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd f₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₃ f₄) h)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂},
  (t₁ ∪ t₂).get k h' = t₁.get k ⋯
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_pred_of_le : ∀ {n : ℕ} (p i : Fin (n + 1)), i ≤ p → ∀ (hi : i ≠ 0), p.succAbove (i.pred hi) = (i.pred hi).castSucc
-- Mathlib.Tactic.FunProp.Core
/-- Try to prove `e` using *composition lambda theorem*.

For example, `e = q(Continuous fun x ↦ f (g x))` and `funPropDecl` is `FunPropDecl` for
`Continuous`

You also have to provide the functions `f` and `g`.  -/
Mathlib.Meta.FunProp.applyCompRule : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    Lean.Expr →
      Lean.Expr →
        (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
          Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.containsThenInsertIfNew_snd : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a parametrized adjunction `F ⊣₂ G` and an arrow `X₁ : Arrow C₁`, this is the induced
adjunction `F.leibnizPushout.obj X₁ ⊣ G.leibnizPullback.obj (op X₁)`.  -/
CategoryTheory.Functor.LeibnizAdjunction.adj : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) →
                (F ⊣₂ G) →
                  (X₁ : CategoryTheory.Arrow C₁) →
                    [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] →
                      [inst_4 : CategoryTheory.Limits.HasPushouts C₃] →
                        F.leibnizPushout.obj X₁ ⊣ G.leibnizPullback.obj (Opposite.op X₁)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.Realize.eq_1 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (φ : L.Formula α) (v : α → M),
  φ.Realize v = FirstOrder.Language.BoundedFormula.Realize φ v default
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- The degree `[L : E]` of `L` over the inertia field `E` equals the ramification index of `p` in `B`.
 -/
IsInertiaField.rank_left : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [FiniteDimensional K L] [inst_8 : MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A]
  [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal]
  (E : Type u_6) [inst_16 : Field E] [inst_17 : Algebra E L] [IsInertiaField K L P E],
  p ≠ ⊥ → Module.finrank E L = p.ramificationIdxIn B
-- Mathlib.Order.Lattice
/-- Transfer `DistribLattice` across an `Equiv`.  -/
Equiv.distribLattice : {α : Type u} → {β : Type v} → α ≃ β → [DistribLattice β] → DistribLattice α
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.LinearEquiv.finsuppUnique.eq_1 : ∀ (R : Type u_1) (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] (α : Type u_5)
  [inst_3 : Unique α],
  Finsupp.LinearEquiv.finsuppUnique R M α =
    { toFun := (Finsupp.equivFunOnFinite.trans (Equiv.funUnique α M)).toFun, map_add' := ⋯, map_smul' := ⋯,
      invFun := (Finsupp.equivFunOnFinite.trans (Equiv.funUnique α M)).invFun, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.exists_restrict_to_vars : ∀ {σ : Type u_1} {s : Set σ} (R : Type u_2) [inst : CommRing R] {F : MvPolynomial σ ℤ},
  ↑F.vars ⊆ s → ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (MvPolynomial.aeval x) F
-- Mathlib.Tactic.ComputeAsymptotics.Lemmas
Tactic.ComputeAsymptotics.isBigO_of_div_tendsto_atBot : ∀ {f g : ℝ → ℝ} {l : Filter ℝ}, Filter.Tendsto (fun x => g x / f x) l Filter.atBot → f =O[l] g
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a non-trivial ring is non-trivial.  -/
Subring.instNontrivialSubtypeMem : ∀ {R : Type u_1} [inst : NonAssocRing R] [Nontrivial R] (s : Subring R), Nontrivial ↥s
-- Mathlib.Algebra.Group.Hom.Defs
instZeroAddHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : AddZeroClass N],
  instZeroAddHom = { zero := { toFun := fun x => 0, map_add' := ⋯ } }
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.nondegenerate_congr_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {B : LinearMap.BilinForm R M} (e : M ≃ₗ[R] M'),
  ((LinearMap.BilinForm.congr e) B).Nondegenerate ↔ B.Nondegenerate
-- Mathlib.RingTheory.DualNumber
TrivSqZeroExt.isUnit_or_isNilpotent : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [inst_4 : SMulCommClass R Rᵐᵒᵖ M] (a : TrivSqZeroExt R M), IsUnit a ∨ IsNilpotent a
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.snd.eq_1 : ∀ (M : Type u_1) (α : Type u_2) (β : Type u_3) [inst : VAdd M α] [inst_1 : VAdd M β],
  AddActionHom.snd M α β = { toFun := Prod.snd, map_vadd' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt16.zero_div : ∀ {a : UInt16}, 0 / a = 0
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm.eq_1 : ∀ {M : Type u_9} {N : Type u_10} [inst : Mul M] [inst_1 : Mul N] (h : M ≃* N),
  h.symm = { toEquiv := h.symm, map_mul' := ⋯ }
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_eq_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = (t.get? a).isSome
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.mem_toConvexCone : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {C : PointedCone R E} {x : E}, x ∈ ↑C ↔ x ∈ C
-- Mathlib.Algebra.Group.Action.End
/-- The tautological action by `MulAut M` on `M`.  -/
MulAut.applyMulAction : {M : Type u_2} → [inst : Monoid M] → MulAction (MulAut M) M
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_subtype_eq_of_support_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {s : Set β},
  Function.support f ⊆ s → ∑' (x : ↑s), f ↑x = ∑' (x : β), f x
-- Mathlib.Data.Quot
Quotient.eq'' : ∀ {α : Sort u_1} {s₁ : Setoid α} {a b : α}, Quotient.mk'' a = Quotient.mk'' b ↔ s₁ a b
-- Init.Meta.Defs
/-- Constructs a typed separated array from elements by adding suitable separators.
The provided array should not include the separators.

Like `Syntax.TSepArray.ofElems` but for untyped syntax.
 -/
Lean.Syntax.SepArray.ofElems : {sep : String} → Array Lean.Syntax → Lean.Syntax.SepArray sep