mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
/-- For `0 < n ≤ m`, the inclusion functor from the `n`-truncated simplex category to the
`m`-truncated simplex category is initial.  -/
SimplexCategory.Truncated.initial_incl : ∀ {n m : ℕ} [NeZero n] (hm : n ≤ m), (SimplexCategory.Truncated.incl n m ⋯).Initial
-- Mathlib.Order.Basic
instLinearOrderEmpty : LinearOrder Empty
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_insert : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] (a : α) (s : Finset α), (insert a s)⁻¹ = insert a⁻¹ s⁻¹
-- Mathlib.CategoryTheory.Quotient
/-- The object of `C`.  -/
CategoryTheory.Quotient.as : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {r : HomRel C} → CategoryTheory.Quotient r → C
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplit.mk.inj : ∀ {pred : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred} {k : ℕ} {h : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof}
  {pred_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred} {k_1 : ℕ}
  {h_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof},
  { pred := pred, k := k, h := h } = { pred := pred_1, k := k_1, h := h_1 } → pred = pred_1 ∧ k = k_1 ∧ h = h_1
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coe_zero : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R], ⇑0 = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblZ_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : Fin 3 → R}, P 2 = 0 → W'.dblZ P = 0
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.id_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (a : α), (CentroidHom.id α) a = a
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
/-- The special-value formula `Γ(k + 1/2) = (2 * k - 1)‼ * √π / (2 ^ k))` for half-integer
values of the gamma function in terms of `Nat.doubleFactorial`.  -/
Real.Gamma_nat_add_half : ∀ (k : ℕ), Real.Gamma (↑k + 1 / 2) = ↑(2 * k - 1).doubleFactorial * √Real.pi / 2 ^ k
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ext_mem_unit : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtDHashMap α fun x => Unit},
  (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁ = m₂
-- Lean.Widget.UserWidget
Lean.Widget.instInhabitedUserWidgetDefinition.default : Lean.Widget.UserWidgetDefinition
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.mk.inj : ∀ {S : Type u_1} {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S} {obj : C}
  {d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj}
  {d_squared :
    autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0)
      CategoryTheory.DifferentialObject.d_squared._autoParam}
  {obj_1 : C} {d_1 : obj_1 ⟶ (CategoryTheory.shiftFunctor C 1).obj obj_1}
  {d_squared_1 :
    autoParam (CategoryTheory.CategoryStruct.comp d_1 ((CategoryTheory.shiftFunctor C 1).map d_1) = 0)
      CategoryTheory.DifferentialObject.d_squared._autoParam},
  { obj := obj, d := d, d_squared := d_squared } = { obj := obj_1, d := d_1, d_squared := d_squared_1 } →
    obj = obj_1 ∧ d ≍ d_1
-- Lean.Parser.Term
Lean.Parser.Term.unreachable.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_scomp_three : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {x : 𝕜},
  ContDiffAt 𝕜 3 g (f x) →
    ContDiffAt 𝕜 3 f x →
      iteratedDeriv 3 (g ∘ f) x =
        deriv f x ^ 3 • iteratedDeriv 3 g (f x) + 3 • iteratedDeriv 2 f x • deriv f x • iteratedDeriv 2 g (f x) +
          iteratedDeriv 3 f x • deriv g (f x)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instFieldSpaceWithValRatFuncWithZeroMultiplicativeIntPolynomialValuationXRatfuncAdicComplPkg : {K : Type u_2} → [inst : Field K] → Field LaurentSeries.ratfuncAdicComplPkg.space
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Composition of `LinearIsometryEquiv`s as a `LinearIsometryEquiv`.  -/
LinearIsometryEquiv.trans : {R : Type u_1} →
  {R₂ : Type u_2} →
    {R₃ : Type u_3} →
      {E : Type u_5} →
        {E₂ : Type u_6} →
          {E₃ : Type u_7} →
            [inst : Semiring R] →
              [inst_1 : Semiring R₂] →
                [inst_2 : Semiring R₃] →
                  {σ₁₂ : R →+* R₂} →
                    {σ₂₁ : R₂ →+* R} →
                      {σ₁₃ : R →+* R₃} →
                        {σ₃₁ : R₃ →+* R} →
                          {σ₂₃ : R₂ →+* R₃} →
                            {σ₃₂ : R₃ →+* R₂} →
                              [inst_3 : RingHomInvPair σ₁₂ σ₂₁] →
                                [inst_4 : RingHomInvPair σ₂₁ σ₁₂] →
                                  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] →
                                    [inst_6 : RingHomInvPair σ₃₁ σ₁₃] →
                                      [inst_7 : RingHomInvPair σ₂₃ σ₃₂] →
                                        [inst_8 : RingHomInvPair σ₃₂ σ₂₃] →
                                          [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                            [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] →
                                              [inst_11 : SeminormedAddCommGroup E] →
                                                [inst_12 : SeminormedAddCommGroup E₂] →
                                                  [inst_13 : SeminormedAddCommGroup E₃] →
                                                    [inst_14 : Module R E] →
                                                      [inst_15 : Module R₂ E₂] →
                                                        [inst_16 : Module R₃ E₃] →
                                                          (E ≃ₛₗᵢ[σ₁₂] E₂) → (E₂ ≃ₛₗᵢ[σ₂₃] E₃) → E ≃ₛₗᵢ[σ₁₃] E₃
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.mapPairIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
  (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.left })
  (g :
    F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.right })
  (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.mapPairIso f g).inv.app X =
    (match X with
      | { as := CategoryTheory.Limits.WalkingPair.left } => f
      | { as := CategoryTheory.Limits.WalkingPair.right } => g).inv
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toArray_toList_ensureTermination : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toList.toArray = it.toArray
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaUncurry_add : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → AddZeroClass (δ i j)] (f g : Π₀ (i : ι) (j : α i), δ i j),
  (f + g).sigmaUncurry = f.sigmaUncurry + g.sigmaUncurry
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.pIntegral_mul : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {x y : ℚ},
  Bernoulli.pIntegral✝ p x → Bernoulli.pIntegral✝ p y → Bernoulli.pIntegral✝ p (x * y)
-- Lean.Meta.IndPredBelow
/-- The names of level parameters  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.levelParams : Lean.Meta.IndPredBelow.Context✝ → List Lean.Name
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.coe_symm_prodEquivOfIsTopCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q),
  ⇑(p.prodEquivOfIsTopCompl q h).symm = ⇑(p.prodEquivOfIsCompl q ⋯).symm
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.negPart : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : AddGroup β] [inst_3 : Lattice β] [ContinuousSup β] [ContinuousNeg β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => (f x)⁻
-- Lean.CoreM
Lean.Core.Context.mk.injEq : ∀ (fileName : String) (fileMap : Lean.FileMap) (options : Lean.Options) (currRecDepth maxRecDepth : ℕ)
  (ref : Lean.Syntax) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (initHeartbeats maxHeartbeats : ℕ)
  (quotContext : Lean.Name) (currMacroScope : Lean.MacroScope) (diag : Bool) (cancelTk? : Option IO.CancelToken)
  (suppressElabErrors : Bool) (inheritedTraceOptions : Std.HashSet Lean.Name) (fileName_1 : String)
  (fileMap_1 : Lean.FileMap) (options_1 : Lean.Options) (currRecDepth_1 maxRecDepth_1 : ℕ) (ref_1 : Lean.Syntax)
  (currNamespace_1 : Lean.Name) (openDecls_1 : List Lean.OpenDecl) (initHeartbeats_1 maxHeartbeats_1 : ℕ)
  (quotContext_1 : Lean.Name) (currMacroScope_1 : Lean.MacroScope) (diag_1 : Bool) (cancelTk?_1 : Option IO.CancelToken)
  (suppressElabErrors_1 : Bool) (inheritedTraceOptions_1 : Std.HashSet Lean.Name),
  ({ fileName := fileName, fileMap := fileMap, options := options, currRecDepth := currRecDepth,
        maxRecDepth := maxRecDepth, ref := ref, currNamespace := currNamespace, openDecls := openDecls,
        initHeartbeats := initHeartbeats, maxHeartbeats := maxHeartbeats, quotContext := quotContext,
        currMacroScope := currMacroScope, diag := diag, cancelTk? := cancelTk?,
        suppressElabErrors := suppressElabErrors, inheritedTraceOptions := inheritedTraceOptions } =
      { fileName := fileName_1, fileMap := fileMap_1, options := options_1, currRecDepth := currRecDepth_1,
        maxRecDepth := maxRecDepth_1, ref := ref_1, currNamespace := currNamespace_1, openDecls := openDecls_1,
        initHeartbeats := initHeartbeats_1, maxHeartbeats := maxHeartbeats_1, quotContext := quotContext_1,
        currMacroScope := currMacroScope_1, diag := diag_1, cancelTk? := cancelTk?_1,
        suppressElabErrors := suppressElabErrors_1, inheritedTraceOptions := inheritedTraceOptions_1 }) =
    (fileName = fileName_1 ∧
      fileMap = fileMap_1 ∧
        options = options_1 ∧
          currRecDepth = currRecDepth_1 ∧
            maxRecDepth = maxRecDepth_1 ∧
              ref = ref_1 ∧
                currNamespace = currNamespace_1 ∧
                  openDecls = openDecls_1 ∧
                    initHeartbeats = initHeartbeats_1 ∧
                      maxHeartbeats = maxHeartbeats_1 ∧
                        quotContext = quotContext_1 ∧
                          currMacroScope = currMacroScope_1 ∧
                            diag = diag_1 ∧
                              cancelTk? = cancelTk?_1 ∧
                                suppressElabErrors = suppressElabErrors_1 ∧
                                  inheritedTraceOptions = inheritedTraceOptions_1)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, s.Finite → t.Finite → (s + t).Finite
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → Inhabited (CategoryTheory.CommComon C)
-- Init.Data.Char.Lemmas
Char.eq_of_val_eq : ∀ {a b : Char}, a.val = b.val → a = b
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.Presieve.regular.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {R : CategoryTheory.Presieve X},
  (∃ Y f, (R = CategoryTheory.Presieve.ofArrows (fun x => Y) fun x => f) ∧ CategoryTheory.EffectiveEpi f) → R.regular
-- Mathlib.Algebra.Group.Action.Defs
VAddAssocClass.op_right : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : VAdd M α] [inst_1 : VAdd M N] [inst_2 : VAdd N α]
  [inst_3 : VAdd Nᵃᵒᵖ α] [IsCentralVAdd N α] [VAddAssocClass M N α], VAddAssocClass M Nᵃᵒᵖ α
-- Mathlib.Analysis.Normed.Module.RCLike.Real
inv_norm_smul_mem_unitClosedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E), ‖x‖⁻¹ • x ∈ Metric.closedBall 0 1
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.instCoeCompletion : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {R : Type u_3} → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Coe R v.Completion
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.norm_dvd_iff : ∀ {S : Type u_1} [inst : CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] {x : S},
  Prime ((Algebra.norm ℤ) x) → ∀ {y : ℤ}, (Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The linear map between the corresponding vector spaces `V1` and `V2`.
This represents how the affine map acts on differences of points.  -/
AffineMap.linear : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] →
                    [inst_5 : Module k V2] → [inst_6 : AddTorsor V2 P2] → (P1 →ᵃ[k] P2) → V1 →ₗ[k] V2
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_eq_of_zero : ∀ {x : ℝ}, ‖↑x‖ = |x|
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_nonneg : ∀ (x : ℝ), 0 ≤ Chebyshev.theta x
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasCtorPattern : Lean.Meta.Match.Problem → Bool
-- Mathlib.Data.FunLike.IsApply
/-- `IsVAddApply M F α β` states for all `f : F`, `n : M` and `x : α`, `(n +ᵥ f) x = n +ᵥ f x`.  -/
IsVAddApply : (M : Type u_1) →
  (F : Type u_2) →
    (α : outParam (Type u_3)) → (β : outParam (Type u_4)) → [FunLike F α β] → [VAdd M β] → [VAdd M F] → Prop
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- Integrals are equal for functions that agree almost everywhere for the restricted measure.  -/
intervalIntegral.integral_congr_ae_restrict : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  f =ᵐ[μ.restrict (Set.uIoc a b)] g → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.evalMonoidHom.eq_1 : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → MulOneClass (f i)] (i : I),
  Pi.evalMonoidHom f i = { toFun := fun g => g i, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber_lt_of_forall_not_threeGPFree : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} {n : ℕ},
  (∀ t ∈ Finset.powersetCard n s, ¬ThreeGPFree ↑t) → mulRothNumber s < n
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a ring homomorphism `f`, the induced homomorphism
on the quotient by `f`'s kernel has the same image as `f`.  -/
RingCon.kerLiftₐ_range_eq : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] {f : M →ₐ[R] P}, (RingCon.kerLiftₐ f).range = f.range
-- Mathlib.Order.Cofinal
IsCofinal.top_mem : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {s : Set α}, IsCofinal s → ⊤ ∈ s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastAppend : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig newWidth) (assign : α → Bool) (idx : ℕ)
  (hidx : idx < newWidth),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend aig target).vec.get idx hidx }⟧ =
    if hr : idx < target.rw then ⟦assign, { aig := aig, ref := target.rhs.get idx hr }⟧
    else
      have this := ⋯;
      ⟦assign, { aig := aig, ref := target.lhs.get (idx - target.rw) ⋯ }⟧
-- Mathlib.Order.RelClasses
instIsTransGe : ∀ {α : Type u} [inst : Preorder α], IsTrans α fun x1 x2 => x2 ≤ x1
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.match_1.eq_6 : ∀ (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) (n₁ : Lean.LMVarId) (k₁ : ℕ) (n₂ : Lean.LMVarId) (k₂ : ℕ)
  (h_1 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂)
  (h_2 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂.succ k₂)
  (h_3 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.max l₁₂ →
        (k₁ : ℕ) → (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.max l₂₂ → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂)
  (h_4 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.imax l₁₂ →
        (k₁ : ℕ) →
          (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.imax l₂₂ → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂)
  (h_5 :
    (n₁ : Lean.Name) →
      (k₁ : ℕ) → (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂)
  (h_6 :
    (n₁ : Lean.LMVarId) →
      (k₁ : ℕ) → (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂)
  (h_7 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂ k₂),
  (match Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ with
    | l₁.succ, k₁, l₂, k₂ => h_1 l₁ k₁ l₂ k₂
    | l₁, k₁, l₂.succ, k₂ => h_2 l₁ k₁ l₂ k₂
    | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_8:(l₂₁.max l₂₂), k₂ => h_3 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_8:(l₂₁.imax l₂₂), k₂ => h_4 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => h_5 n₁ k₁ n₂ k₂
    | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ => h_6 n₁ k₁ n₂ k₂
    | l₁, k₁, l₂, k₂ => h_7 l₁ k₁ l₂ k₂) =
    h_6 n₁ k₁ n₂ k₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.shouldPreprocess : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Combinatorics.SimpleGraph.Basic
completeBipartiteGraph_adj : ∀ (V : Type u_1) (W : Type u_2) (v w : V ⊕ W),
  (completeBipartiteGraph V W).Adj v w = (v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true)
-- Mathlib.Order.DirectedInverseSystem
/-- The direct limit of a directed system.  -/
DirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (F : ι → Type u_4) →
      {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} →
        (f : (i j : ι) → (h : i ≤ j) → T h) →
          [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] →
            [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] → [IsDirectedOrder ι] → Type (max u_4 u_1)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
continuousWithinAt_iff_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_7} [inst_6 : TopologicalSpace M'] {f : M → M'}
  {s : Set M} {x : M},
  ContinuousWithinAt f s x ↔
    ContinuousWithinAt (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] [inst_3 : Inhabited α] {l : List α} {k : α},
  k ∉ t → l.contains k = false → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKey! k = default
-- Batteries.Data.List.Basic
List.tails.eq_1 : ∀ {α : Type u_1}, [].tails = [[]]
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
/-- The orbit map `g ↦ g • I` is a proper map `SL(2, ℝ) → ℍ`.  -/
UpperHalfPlane.isProperMap_smul_I : IsProperMap fun g => g • UpperHalfPlane.I
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- `MulAlgebraNormClass F R S` states that `F` is a type of multiplicative `R`-algebra norms on
the ring `S`. You should extend this class when you extend `MulAlgebraNorm`.  -/
MulAlgebraNormClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    [inst : SeminormedCommRing R] →
      (S : outParam (Type u_3)) → [inst_1 : Ring S] → [Algebra R S] → [FunLike F S ℝ] → Prop
-- Mathlib.Control.Monad.Cont
LawfulMonadCont.mk : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : MonadCont m] [toLawfulMonad : LawfulMonad m],
  (∀ {α ω γ : Type u} (cmd : m α) (next : MonadCont.Label ω m γ → α → m ω),
      (MonadCont.callCC fun f => cmd >>= next f) = do
        let x ← cmd
        MonadCont.callCC fun f => next f x) →
    (∀ {α : Type u} (β : Type u) (x : α) (dead : MonadCont.Label α m β → β → m α),
        (MonadCont.callCC fun f => MonadCont.goto f x >>= dead f) = pure x) →
      (∀ {α β : Type u} (dummy : m α), (MonadCont.callCC fun x => dummy) = dummy) → LawfulMonadCont m
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.iSup_adjoin_eq_top : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E],
  ⨆ i,
      IntermediateField.adjoin F
        (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i) =
    ⊤
-- Std.Async.Process
Std.IO.Process.instInhabitedPId.default : Std.IO.Process.PId
-- Aesop.Forward.RuleInfo
/-- The forward dependencies of this slot. These are all the premises that
appear in slots *after* this one.  -/
Aesop.Slot.forwardDeps : Aesop.Slot → Array Aesop.PremiseIndex
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.homMk_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommMon C} (f : A.toMon ⟶ B.toMon),
  (CategoryTheory.CommMon.homMk f).hom = f
-- Mathlib.LinearAlgebra.Transvection.Generation
/-- A linear equivalence `u : V ≃ₗ[K] V` is exceptional if
it is a nontrivial homothety modulo `u.fixedSubmodule`.  -/
LinearEquiv.IsExceptional : {K : Type u_1} →
  [inst : DivisionRing K] → {V : Type u_2} → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → (V ≃ₗ[K] V) → Prop
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.equiv_symm_apply : ∀ (a : ℂ), CliffordAlgebraComplex.equiv.symm a = CliffordAlgebraComplex.ofComplex a
-- Mathlib.Algebra.Star.Pointwise
Set.star_mem_star : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : InvolutiveStar α], star a ∈ star s ↔ a ∈ s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_of_contains_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  (t.insert k).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.comp_isOpenMap_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) {f : Z → X}, IsOpenMap (⇑h ∘ f) ↔ IsOpenMap f