mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Ergodic.Conservative
MeasureTheory.Conservative.congr_ae : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ ν : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ → MeasureTheory.ae μ = MeasureTheory.ae ν → MeasureTheory.Conservative f ν
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_ofNat : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {f : σ → R} (n : ℕ) [inst_1 : n.AtLeastTwo],
  (MvPolynomial.eval f) (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Order.OrderDual
OrderDual.lt_toDual : ∀ {α : Type u_1} [inst : LT α] {a : αᵒᵈ} {b : α}, a < OrderDual.toDual b ↔ b < OrderDual.ofDual a
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.toNat.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (a : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.negSucc a with
    | Int.ofNat n => h_1 n
    | Int.negSucc a => h_2 a) =
    h_2 a
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_intCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (z : ℤ), (↑z).imI = 0
-- Mathlib.RepresentationTheory.Basic
Representation.instInhabitedAsModule : {k : Type u_4} →
  {G : Type u_5} →
    {V : Type u_6} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → (ρ : Representation k G V) → Inhabited ρ.asModule
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.flip_inr : ∀ {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₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂), sq.flip.inr = sq.inl
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.instLawfulVecOperatorTwoPowShiftTargetTwoPowShift : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift
-- Mathlib.Algebra.Category.CommAlgCat.Basic
_private.Mathlib.Algebra.Category.CommAlgCat.Basic.0.CommAlgCat.mk : {R : Type u} →
  [inst : CommRing R] →
    (carrier : Type v) → [commRing : CommRing carrier] → [algebra : Algebra R carrier] → CommAlgCat R
-- Mathlib.Topology.EMetricSpace.Defs
Metric.mem_eball_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, 0 < ε → x ∈ Metric.eball x ε
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The canonical map from the multiequalizer to the objects on the left.  -/
CategoryTheory.Limits.Multiequalizer.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] →
          (a : J.L) → CategoryTheory.Limits.multiequalizer I ⟶ I.left a
-- Mathlib.Algebra.Star.Pi
Function.update_star : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Star (f i)] [inst_1 : DecidableEq I] (h : (i : I) → f i) (i : I)
  (a : f i), Function.update (star h) i (star a) = star (Function.update h i a)
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNorm'_const_smul_le : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} {𝕜 : Type u_3} [inst_1 : NormedRing 𝕜] [inst_2 : MulActionWithZero 𝕜 F]
  [IsBoundedSMul 𝕜 F] {c : 𝕜}, 0 < q → MeasureTheory.eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * MeasureTheory.eLpNorm' f q μ
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.instFromJsonCallHierarchy.fromJson : Lean.Json → Except String Lean.Lsp.Ipc.CallHierarchy
-- Mathlib.Logic.Equiv.Defs
/-- The sort of maps from `True` is equivalent to the codomain.  -/
Equiv.trueArrowEquiv : (α : Sort u_1) → (True → α) ≃ α
-- Mathlib.Algebra.Polynomial.Div
Polynomial.pow_rootMultiplicity_not_dvd : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R},
  p ≠ 0 → ∀ (a : R), ¬(Polynomial.X - Polynomial.C a) ^ (Polynomial.rootMultiplicity a p + 1) ∣ p
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_ofNat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocMod hp a (b - OfNat.ofNat m * p) = toIocMod hp a b
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.step_invRev_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeGroup.Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ FreeGroup.Red.Step L₁ L₂
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.sub_mem : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) {x y : L}, x ∈ L' → y ∈ L' → x - y ∈ L'
-- Mathlib.Topology.Algebra.Star
/-- Basic hypothesis to talk about a topological space with a continuous `star` operator.  -/
ContinuousStar : (R : Type u_1) → [TopologicalSpace R] → [Star R] → Prop
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ιOrZero_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ⋯ = j),
  ⋯ = ⋯
-- Mathlib.Data.ENNReal.Basic
ENNReal.instIsOrderedAddMonoid : IsOrderedAddMonoid ENNReal
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.zero.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.zero = H.zero
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- A variant of the normalization functor where we consider the result as an object in the free
monoidal category (rather than an object of the discrete subcategory of objects in normal form).  -/
CategoryTheory.FreeMonoidalCategory.normalize' : (C : Type u) →
  CategoryTheory.Functor (CategoryTheory.FreeMonoidalCategory C)
    (CategoryTheory.Functor ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
      (CategoryTheory.FreeMonoidalCategory C))
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_subgroupOf_sup_of_le_normalizer : ∀ {G : Type u_1} [inst : Group G] {H N : Subgroup G}, H ≤ Subgroup.normalizer ↑N → (N.subgroupOf (H ⊔ N)).Normal
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₁.RightHomologyData)
  (h₁' : S₂.LeftHomologyData) (h₂' : S₂.RightHomologyData),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₁')
      (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)
      (CategoryTheory.ShortComplex.rightHomologyMap' φ h₂ h₂')
-- Init.Data.Vector.Attach
Vector.pmap_attach : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {p : { x // x ∈ xs } → Prop}
  {f : (a : { x // x ∈ xs }) → p a → β} (H : ∀ a ∈ xs.attach, p a),
  Vector.pmap f xs.attach H = Vector.pmap (fun a h => f ⟨a, ⋯⟩ ⋯) xs ⋯
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (b a : α) [inst_2 : Fintype ↑(Set.Ioc b a)],
  Fintype.card ↑(Set.Ioc b a) = (Finset.Ioc b a).card
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_whiskerRight_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] {X Y : C} (f : X ⟶ Y) (Z : C) {Z_1 : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y Z) h))
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.functorHom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {X : C} {x y : (F.functorHom G).obj X},
  x = y ↔ ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If `P` is a sheaf for `S`, and it is iso to `P'`, then `P'` is a sheaf for `S`. This shows that
"being a sheaf for a presieve" is a mathematical or hygienic property.
 -/
CategoryTheory.Presieve.isSheafFor_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} {P' : CategoryTheory.Functor Cᵒᵖ (Type w)} (i : P ≅ P'),
  CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSheafFor P' R
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv.congr_simp : ∀ {R : Type u_5} [inst : CommRing R] (S : Submonoid R) (P : Type u_6) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (P' : Type u_7) [inst_3 : CommRing P'] [inst_4 : Algebra R P'] [inst_5 : IsLocalization S P]
  [inst_6 : IsLocalization S P'], FractionalIdeal.canonicalEquiv S P P' = FractionalIdeal.canonicalEquiv S P P'
-- Init.Data.Format.Syntax
_private.Init.Data.Format.Syntax.0.Lean.Syntax.formatInfo : Bool → Lean.SourceInfo → Std.Format → Std.Format
-- Lean.Parser.Command
Lean.Parser.Command.dumpAsyncEnvState.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instNormal : ∀ {G : Type u_1} [inst : AddGroup G] (H : FiniteIndexNormalAddSubgroup G), H.Normal
-- Mathlib.Order.RelIso.Basic
RelEmbedding.acc : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (a : α), Acc s (f a) → Acc r a
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_le : ∀ {a b : UInt64}, a.toUInt32 ≤ b.toUInt32 ↔ a % 4294967296 ≤ b % 4294967296
-- Lean.Data.Name
Lean.Name.componentsRev : Lean.Name → List Lean.Name
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_sup_units : ∀ {M : Type u_1} [inst : Monoid M] (S T : Subgroup Mˣ), (S.ofUnits ⊔ T.ofUnits).units = S ⊔ T
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.one_toGerm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : One β], MeasureTheory.AEEqFun.toGerm 1 = 1
-- Mathlib.Analysis.Convex.Approximation
/-- The sequential version of `univ_sSup_of_countable_affine_eq`.  -/
ConvexOn.univ_sSup_of_nat_affine_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  LowerSemicontinuous φ →
    ConvexOn ℝ Set.univ φ →
      ∃ l c,
        (∀ (i : ℕ), ⇑RCLike.re ∘ ⇑(l i) + Function.const E (c i) ≤ φ) ∧
          ⨆ i, ⇑RCLike.re ∘ ⇑(l i) + Function.const E (c i) = φ
-- Batteries.Tactic.GeneralizeProofs
/-- Elaborates a `Parser.Tactic.config` for `generalize_proofs`.  -/
Batteries.Tactic.GeneralizeProofs.elabConfig : Lean.Syntax →
  optParam Batteries.Tactic.GeneralizeProofs.Config { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Batteries.Tactic.GeneralizeProofs.Config
-- Init.Data.Nat.Basic
Nat.add_one_le_add_one_iff : ∀ {a b : ℕ}, a + 1 ≤ b + 1 ↔ a ≤ b
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.src_eq : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Edge x₀ x₁),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) e.edge = x₀
-- Mathlib.Computability.Partrec
Nat.Partrec.of_primrec : ∀ {f : ℕ → ℕ}, Nat.Primrec f → Nat.Partrec ↑f
-- Init.Data.Vector.Lemmas
Vector.replace_replicate_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {b a : α} (h : 0 < n),
  (Vector.replicate n a).replace a b = Vector.cast ⋯ (#v[b] ++ Vector.replicate (n - 1) a)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
independent.  -/
Module.End.eigenvectors_linearIndependent' : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_1}
  [IsDomain R] [Module.IsTorsionFree R M] (f : Module.End R M) (μ : ι → R),
  Function.Injective μ → ∀ (v : ι → M), (∀ (i : ι), f.HasEigenvector (μ i) (v i)) → LinearIndependent R v
-- Lean.Meta.Basic
Lean.Meta.Config.mk.inj : ∀
  {foApprox ctxApprox quasiPatternApprox constApprox isDefEqStuckEx unificationHints proofIrrelevance
    assignSyntheticOpaque offsetCnstrs : Bool}
  {transparency : Lean.Meta.TransparencyMode} {etaStruct : Lean.Meta.EtaStructMode} {univApprox iota beta : Bool}
  {proj : Lean.Meta.ProjReductionKind}
  {zeta zetaDelta zetaUnused zetaHave foApprox_1 ctxApprox_1 quasiPatternApprox_1 constApprox_1 isDefEqStuckEx_1
    unificationHints_1 proofIrrelevance_1 assignSyntheticOpaque_1 offsetCnstrs_1 : Bool}
  {transparency_1 : Lean.Meta.TransparencyMode} {etaStruct_1 : Lean.Meta.EtaStructMode}
  {univApprox_1 iota_1 beta_1 : Bool} {proj_1 : Lean.Meta.ProjReductionKind}
  {zeta_1 zetaDelta_1 zetaUnused_1 zetaHave_1 : Bool},
  { foApprox := foApprox, ctxApprox := ctxApprox, quasiPatternApprox := quasiPatternApprox, constApprox := constApprox,
        isDefEqStuckEx := isDefEqStuckEx, unificationHints := unificationHints, proofIrrelevance := proofIrrelevance,
        assignSyntheticOpaque := assignSyntheticOpaque, offsetCnstrs := offsetCnstrs, transparency := transparency,
        etaStruct := etaStruct, univApprox := univApprox, iota := iota, beta := beta, proj := proj, zeta := zeta,
        zetaDelta := zetaDelta, zetaUnused := zetaUnused, zetaHave := zetaHave } =
      { foApprox := foApprox_1, ctxApprox := ctxApprox_1, quasiPatternApprox := quasiPatternApprox_1,
        constApprox := constApprox_1, isDefEqStuckEx := isDefEqStuckEx_1, unificationHints := unificationHints_1,
        proofIrrelevance := proofIrrelevance_1, assignSyntheticOpaque := assignSyntheticOpaque_1,
        offsetCnstrs := offsetCnstrs_1, transparency := transparency_1, etaStruct := etaStruct_1,
        univApprox := univApprox_1, iota := iota_1, beta := beta_1, proj := proj_1, zeta := zeta_1,
        zetaDelta := zetaDelta_1, zetaUnused := zetaUnused_1, zetaHave := zetaHave_1 } →
    foApprox = foApprox_1 ∧
      ctxApprox = ctxApprox_1 ∧
        quasiPatternApprox = quasiPatternApprox_1 ∧
          constApprox = constApprox_1 ∧
            isDefEqStuckEx = isDefEqStuckEx_1 ∧
              unificationHints = unificationHints_1 ∧
                proofIrrelevance = proofIrrelevance_1 ∧
                  assignSyntheticOpaque = assignSyntheticOpaque_1 ∧
                    offsetCnstrs = offsetCnstrs_1 ∧
                      transparency = transparency_1 ∧
                        etaStruct = etaStruct_1 ∧
                          univApprox = univApprox_1 ∧
                            iota = iota_1 ∧
                              beta = beta_1 ∧
                                proj = proj_1 ∧
                                  zeta = zeta_1 ∧
                                    zetaDelta = zetaDelta_1 ∧ zetaUnused = zetaUnused_1 ∧ zetaHave = zetaHave_1
-- Mathlib.Order.Basic
LE.le.le_or_gt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, b ≤ a → ∀ (c : α), c ≤ a ∨ b < c
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_min : ∀ {G : Type u} [inst : AddMonoid G] (m : ℕ), 0 < m → m < AddMonoid.exponent G → ∃ g, m • g ≠ 0
-- Mathlib.Data.Fintype.Order
Finite.ciSup_mono : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] [inst : ConditionallyCompleteLattice α] {f g : ι → α},
  (∀ (x : ι), f x ≤ g x) → iSup f ≤ iSup g
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverTerms.next.sizeOf_spec : ∀ (solverId : ℕ) (e : Lean.Expr) (rest : Lean.Meta.Grind.SolverTerms),
  sizeOf (Lean.Meta.Grind.SolverTerms.next solverId e rest) = 1 + sizeOf solverId + sizeOf e + sizeOf rest
-- Mathlib.Order.Monotone.Monovary
Monovary.symm : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Monovary f g → Monovary g f
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.max_ne : ∀ {R : Type u_2} [inst : LinearOrder R] {a b c : R}, a ≠ c → b ≠ c → max a b ≠ c
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain_add : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (x y : MonoidAlgebra R M),
  MonoidAlgebra.mapDomain f (x + y) = MonoidAlgebra.mapDomain f x + MonoidAlgebra.mapDomain f y
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (H' :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H') f = g
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.instInhabited : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} →
            {h₂ : S₂.HomologyData} → Inhabited (CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
-- Lean.Parser.Command
Lean.Parser.Command.private.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.descCocycle_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cocycle G K n) (h : m + 1 = n)
  (eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯),
  ↑(CochainComplex.mappingCone.descCocycle φ α β h eq) = CochainComplex.mappingCone.descCochain φ α (↑β) h
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom_apply : ∀ (X Y : Type u) (x : Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom)
      ((CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.coprod.inr) x) =
    Sum.inr x
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGE_iff_getElem_ge_getElem_of_le`. -/
List.SortedGE.getElem_ge_getElem_of_le : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  l.SortedGE → ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j ≤ i → l[i] ≤ l[j]
-- Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
/-- **Dominated convergence theorem** for nonnegative `Measurable` functions.  -/
MeasureTheory.tendsto_lintegral_of_dominated_convergence : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal}
  (bound : α → ENNReal),
  (∀ (n : ℕ), Measurable (F n)) →
    (∀ (n : ℕ), F n ≤ᵐ[μ] bound) →
      ∫⁻ (a : α), bound a ∂μ ≠ ⊤ →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
          Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Construct a natural isomorphism between functors out of a walking multicospan from its
components.  -/
CategoryTheory.Limits.WalkingMulticospan.functorExt : {J : CategoryTheory.Limits.MulticospanShape} →
  {C : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan J) C} →
        (left :
            (i : J.L) →
              F.obj (CategoryTheory.Limits.WalkingMulticospan.left i) ≅
                G.obj (CategoryTheory.Limits.WalkingMulticospan.left i)) →
          (right :
              (i : J.R) →
                F.obj (CategoryTheory.Limits.WalkingMulticospan.right i) ≅
                  G.obj (CategoryTheory.Limits.WalkingMulticospan.right i)) →
            autoParam
                (∀ (i : J.R),
                  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i))
                      (right i).hom =
                    CategoryTheory.CategoryStruct.comp (left (J.fst i)).hom
                      (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i)))
                CategoryTheory.Limits.WalkingMulticospan.functorExt._auto_1 →
              autoParam
                  (∀ (i : J.R),
                    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i))
                        (right i).hom =
                      CategoryTheory.CategoryStruct.comp (left (J.snd i)).hom
                        (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)))
                  CategoryTheory.Limits.WalkingMulticospan.functorExt._auto_3 →
                (F ≅ G)
-- Mathlib.Analysis.RCLike.Basic
RCLike.mul_im : ∀ {K : Type u_1} [inst : RCLike K] (z w : K), RCLike.im (z * w) = RCLike.re z * RCLike.im w + RCLike.im z * RCLike.re w
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.insert.match_1.eq_1 : ∀ (motive : RBTree.RBColor → Sort u_1) (h_1 : Unit → motive RBTree.RBColor.red)
  (h_2 : Unit → motive RBTree.RBColor.black),
  (match RBTree.RBColor.red with
    | RBTree.RBColor.red => h_1 ()
    | RBTree.RBColor.black => h_2 ()) =
    h_1 ()
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n