mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.full_arrow_eq_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (D : Set C) {c d : ↑(CategoryTheory.Subgroupoid.full D).objs}
  {f g : c ⟶ d}, f = g ↔ ↑f = ↑g
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.of_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  {W' : CategoryTheory.MorphismProperty C} [W.HasOfPrecompProperty W'] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  W' f → W (CategoryTheory.CategoryStruct.comp f g) → W g
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_5.eq : ∀ {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_2 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Sort u}
  {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u}
  {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u}
  (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot))
  (F_1 : (t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t :
        Lean.Language.TransformedSnap
          (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t)
  (F_5 :
    (t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t)
  (F_6 :
    (t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t)
  (F_7 :
    (t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
      Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t)
  (F_8 :
    (t : Task Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t),
  Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_5 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 =
    F_6 t (Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_5.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8).2
-- Mathlib.Algebra.Lie.TensorProduct
/-- It is useful to define the bracket via this auxiliary function so that we have a type-theoretic
expression of the fact that `L` acts by linear endomorphisms. It simplifies the proofs in
`lieRingModule` below.  -/
TensorProduct.LieModule.hasBracketAux : {R : Type u} →
  [inst : CommRing R] →
    {L : Type v} →
      {M : Type w} →
        {N : Type w₁} →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [inst_5 : LieRingModule L M] →
                    [LieModule R L M] →
                      [inst_7 : AddCommGroup N] →
                        [inst_8 : Module R N] →
                          [inst_9 : LieRingModule L N] → [LieModule R L N] → L → Module.End R (TensorProduct R M N)
-- Lean.Declaration
Lean.ReducibilityHints.abbrev : Lean.ReducibilityHints
-- Init.Data.List.Find
List.find?_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} {p : β → Bool},
  List.find? p (List.flatMap f xs) = List.findSome? (fun x => List.find? p (f x)) xs
-- Mathlib.Geometry.Manifold.PartitionOfUnity
BumpCovering.IsSubordinate.toSmoothPartitionOfUnity : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} {f : BumpCovering ι M s} {U : ι → Set M},
  f.IsSubordinate U →
    ∀ (hf : ∀ (i : ι), ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ ⇑(f i)),
      (f.toSmoothPartitionOfUnity hf).IsSubordinate U
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α], List.Pairwise (fun a b => a < b) r.toList
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_elim_cert : ℤ → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → Bool
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor_map : ∀ (Y : AlgebraicGeometry.Scheme) {I J : Y.IdealSheafDataᵒᵖ} (h : I ⟶ J),
  (AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor Y).map h =
    CategoryTheory.Over.homMk (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯) ⋯
-- Lean.Elab.Tactic.RCases
/-- An explicit pattern `@pat`.  -/
Lean.Elab.Tactic.RCases.RCasesPatt.explicit : Lean.Syntax → Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt
-- Mathlib.NumberTheory.NumberField.Norm
RingOfIntegers.algebraMap_norm_algebraMap : ∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (x : NumberField.RingOfIntegers K),
  (algebraMap (NumberField.RingOfIntegers K) K)
      ((RingOfIntegers.norm K) ((algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) x)) =
    (Algebra.norm K) ((algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) x))
-- Mathlib.Data.Finset.Prod
Finset.union_product : ∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t : Finset β} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t
-- Init.Data.Slice.List.Iterator
List.instAppendListSlice : {α : Type u} → Append (ListSlice α)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
spectrum_nonneg_of_nonneg : ∀ {𝕜 : Type u_3} {A : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Ring A]
  [inst_3 : PartialOrder A] [inst_4 : Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] ⦃a : A⦄,
  0 ≤ a → ∀ ⦃x : 𝕜⦄, x ∈ spectrum 𝕜 a → 0 ≤ x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_some_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  (h' : a ∈ m), m[a]? = some m[a]
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_id'' : ∀ {α : Type u_1} {m mα : MeasurableSpace α}, m ≤ mα → Measurable id
-- Mathlib.Computability.Encoding
/-- An `Encoding` of a `List α` in alphabet `α`, encoded directly.  -/
Computability.encodingList : (α : Type) → Computability.Encoding (List α) α
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_strictMono : StrictMono Nat.fermatNumber
-- Batteries.Tactic.Lint.Frontend
/-- Sorts a map with declaration keys as names by line number.  -/
Batteries.Tactic.Lint.sortResults : {α : Type} → Std.HashMap Lean.Name α → Lean.CoreM (Array (Lean.Name × α))
-- Mathlib.Data.List.DropRight
List.rtakeWhile_eq_nil_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given `P : Cᵒᵖ ⥤ Type max w v₁`, this is the functor from the opposite category
of the category of elements of `X` which sends an element in `P.obj (op X)` to the
presheaf represented by `X`. The definition `coconeOfRepresentable`
gives a cocone for this functor which is a colimit and has point `P`.
 -/
CategoryTheory.Presheaf.functorToRepresentables : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) →
      CategoryTheory.Functor P.Elementsᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁)))
-- Mathlib.GroupTheory.Congruence.Opposite
/-- If `c` is an additive congruence on `M`, then `(a, b) ↦ c b.unop a.unop` is an
additive congruence on `Mᵃᵒᵖ`  -/
AddCon.op : {M : Type u_1} → [inst : Add M] → AddCon M → AddCon Mᵃᵒᵖ
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.instHasCokernelsFullSubcategoryOfIsClosedUnderCokernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderCokernels] [CategoryTheory.Limits.HasCokernels C],
  CategoryTheory.Limits.HasCokernels P.FullSubcategory
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.natTrailingDegree = p.trailingDegree.toNat
-- Mathlib.Order.DirSupClosed
dirSupClosed_Iic : ∀ {α : Type u_1} [inst : Preorder α] (a : α), DirSupClosed (Set.Iic a)
-- Mathlib.Topology.Constructible
IsRetrocompact.iUnion : ∀ {ι : Sort u_1} {X : Type u_2} [inst : TopologicalSpace X] [Finite ι] {f : ι → Set X},
  (∀ (i : ι), IsRetrocompact (f i)) → IsRetrocompact (⋃ i, f i)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.div_rpow : ∀ (x y : NNReal) (z : ℝ), (x / y) ^ z = x ^ z / y ^ z
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.sep_subset_ofPred`. -/
Set.sep_subset_setOf : ∀ {α : Type u} (s : Set α) (p : α → Prop), {x | x ∈ s ∧ p x} ⊆ {x | p x}
-- Mathlib.Topology.CWComplex.Classical.Basic
_private.Mathlib.Topology.CWComplex.Classical.Basic.0.Topology.CWComplex.OfDiscreteClosed.match_3.eq_1 : ∀ {X : Type u_1} {D : Set X}
  (motive :
    (n : ℕ) →
      (match n with
        | 0 => ↑D
        | n.succ => PEmpty.{u_1 + 1}) →
        Sort u_2)
  (i :
    match 0 with
    | 0 => ↑D
    | n.succ => PEmpty.{u_1 + 1})
  (h_1 :
    (i :
        match 0 with
        | 0 => ↑D
        | n.succ => PEmpty.{u_1 + 1}) →
      motive 0 i)
  (h_2 :
    (n : ℕ) →
      (i :
          match n + 1 with
          | 0 => ↑D
          | n.succ => PEmpty.{u_1 + 1}) →
        motive n.succ i),
  (match 0, i with
    | 0, i => h_1 i
    | n.succ, i => h_2 n i) =
    h_1 i
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.coe_def : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : FiniteDimensional ℝ E] {c : M} (f : SmoothBumpFunction I c),
  ↑f = (chartAt H c).source.indicator (↑f.toContDiffBump ∘ ↑(extChartAt I c))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.map_map_equiv : ∀ {α : Type u} {β : Type v} {γ δ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → γ}
  {g : α → γ → δ}, (Std.TreeMap.map g (Std.TreeMap.map f t)).Equiv (Std.TreeMap.map (fun k v => g k (f k v)) t)
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The functor taking a representation `rep` to the representation `C(G, rep)`.
The `G` action is defined by `g • f := x ↦ g • f (g⁻¹ * x)`.  -/
TopRep.coind₁Functor : (k : Type u) →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] →
      (G : Type v) →
        [inst_2 : Group G] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → CategoryTheory.Functor (TopRep k G) (TopRep k G)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.instMembershipForallReal : {ι : Type u_1} → Membership (ι → ℝ) (BoxIntegral.Box ι)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.equivalence_functor_obj_coe : ∀ (X : AddCommMonCat), ↑(AddCommMonCat.equivalence.functor.obj X) = Multiplicative ↑X
-- Mathlib.Lean.FoldEnvironment
/-- Run `act env name constInfo`, catching potential errors.  -/
_private.Mathlib.Lean.FoldEnvironment.0.Lean.Meta.visitConst : {α : Type} →
  Lean.Name →
    Lean.Meta.FoldDeclErrorRef →
      (α → Lean.Name → Lean.ConstantInfo → Lean.MetaM α) → α → Lean.Name → Lean.ConstantInfo → Lean.MetaM α
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.fac_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) [hsq : sq.HasLift], CategoryTheory.CategoryStruct.comp i sq.lift = f
-- Std.Data.Iterators.Consumers.Set
/-- Traverses the given iterator and stores the emitted values in a {name}`ExtTreeSet`.

If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α Id`,
the variant {lean}`it.ensureTermination.toExtTreeSet cmp` always terminates after finitely many steps.
 -/
Std.Iter.toExtTreeSet : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.IteratorLoop α Id Id] →
      Std.Iter β →
        (cmp : autoParam (β → β → Ordering) Std.Iter.toExtTreeSet._auto_1) → [Std.TransCmp cmp] → Std.ExtTreeSet β cmp
-- Mathlib.Data.Finset.Lattice.Basic
Finset.forall_mem_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {p : α → Prop},
  (∀ a ∈ s ∪ t, p a) ↔ (∀ a ∈ s, p a) ∧ ∀ a ∈ t, p a
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- `PolynomialModule.coeff` as a linear equiv.  -/
PolynomialModule.coeffLinearEquiv : (R : Type u_2) →
  {M : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (S : Type u_5) → [inst_3 : CommSemiring S] → [inst_4 : Module S M] → PolynomialModule R M ≃ₗ[S] ℕ →₀ M
-- Mathlib.Order.Heyting.Hom
HeytingHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : HeytingAlgebra α} {inst_1 : HeytingAlgebra β} {toLatticeHom : LatticeHom α β}
  {map_bot' : toLatticeHom.toFun ⊥ = ⊥}
  {map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b}
  {toLatticeHom_1 : LatticeHom α β} {map_bot'_1 : toLatticeHom_1.toFun ⊥ = ⊥}
  {map_himp'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a ⇨ b) = toLatticeHom_1.toFun a ⇨ toLatticeHom_1.toFun b},
  { toLatticeHom := toLatticeHom, map_bot' := map_bot', map_himp' := map_himp' } =
      { toLatticeHom := toLatticeHom_1, map_bot' := map_bot'_1, map_himp' := map_himp'_1 } →
    toLatticeHom = toLatticeHom_1
-- Init.Data.Vector.Lemmas
Vector.toArray_pop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.pop.toArray = xs.toArray.pop
-- Std.Time.Time.Unit.Millisecond
/-- Creates an `Ordinal` from an integer, ensuring the value is within bounds.
 -/
Std.Time.Millisecond.Ordinal.ofInt : (data : ℤ) → 0 ≤ data ∧ data ≤ 999 → Std.Time.Millisecond.Ordinal
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Units.val_inv_cfcRpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : Aˣ) (x : ℝ) (ha : autoParam (0 ≤ ↑a) Units.cfcRpow._auto_1),
  ↑(a.cfcRpow x ha)⁻¹ = ↑a ^ (-x)
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_3.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} (t : Array (Lean.Doc.Block i b))
  (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  Lean.Doc.Block.brecOn_3 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_4 t (Lean.Doc.Block.brecOn_3.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
MvQPF.Comp.instInhabited : {n m : ℕ} →
  {F : TypeVec.{u} n → Type u_1} →
    {G : Fin2 n → TypeVec.{u} m → Type u} →
      {α : TypeVec.{u} m} → [I : Inhabited (F fun i => G i α)] → Inhabited (MvQPF.Comp F G α)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.mem_eball`. -/
EMetric.mem_ball : ∀ {α : Type u} [inst : EDist α] {x y : α} {ε : ENNReal}, y ∈ Metric.eball x ε ↔ edist y x < ε
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects finite coproducts, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite
products.  -/
CategoryTheory.Limits.reflectsFiniteProducts_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteCoproducts F],
  CategoryTheory.Limits.ReflectsFiniteProducts F.op
-- Std.Time.DateTime.PlainDateTime
/-- The `Time` component of a `PlainTime`
 -/
Std.Time.PlainDateTime.time : Std.Time.PlainDateTime → Std.Time.PlainTime
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_right_unitality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Modules.pullbackComp (CategoryTheory.CategoryStruct.id X) f).inv
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.Scheme.Modules.pullback f).whiskerLeft (AlgebraicGeometry.Scheme.Modules.pullbackId X).hom)
        (AlgebraicGeometry.Scheme.Modules.pullback f).rightUnitor.hom) =
    CategoryTheory.eqToHom ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub
Std.Tactic.BVDecide.BVExpr.bitblast.blastSub.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastSub aig { lhs := lhs, rhs := rhs } =
    Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd (Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg aig rhs).aig
      { lhs := lhs.cast ⋯, rhs := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNeg aig rhs).vec }
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.map_obj : ∀ {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) (U : TopologicalSpace.Opens ↑Y)
  (q : (CategoryTheory.ConcreteCategory.hom f) x ∈ U),
  (TopologicalSpace.OpenNhds.map f x).obj ⟨U, q⟩ = ⟨(TopologicalSpace.Opens.map f).obj U, q⟩
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Adds hNames to the local context to reserve their names and runs `m` in that context.  -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabAppMatch.withDummyBinders : {α : Type} →
  Array (Option Lean.Name) →
    Lean.Expr →
      (Array (Option Lean.Name) → Lean.PrettyPrinter.Delaborator.DelabM α) →
        optParam (Array (Option Lean.Name)) #[] → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.AlgebraicGeometry.Group.Affine
CategoryTheory.over.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X S : C) (x : CategoryTheory.OverClass X S),
  CategoryTheory.over X S x = CategoryTheory.OverClass.hom
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {fallback : α}, t.getD t.max! fallback = t.max!
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.equiv_of_beq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α]
  [inst_1 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)], (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The natural transformation `π₁ ⟶ π₂` induced by `S.f` for all `S : ShortComplex C`.  -/
CategoryTheory.ShortComplex.π₁Toπ₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.ShortComplex.π₁ ⟶ CategoryTheory.ShortComplex.π₂
-- Mathlib.Topology.Algebra.MulAction
instContinuousVAddForall_1 : ∀ {ι : Type u_5} {γ : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (γ i)] {N : ι → Type u_7}
  [inst_1 : (i : ι) → TopologicalSpace (N i)] [inst_2 : (i : ι) → VAdd (N i) (γ i)]
  [∀ (i : ι), ContinuousVAdd (N i) (γ i)], ContinuousVAdd ((i : ι) → N i) ((i : ι) → γ i)
-- Mathlib.Data.Finset.Defs
Finset.instDecidableLE : {α : Type u_1} → [DecidableEq α] → DecidableLE (Finset α)
-- Mathlib.Data.PEquiv
PEquiv.mk.congr_simp : ∀ {α : Type u} {β : Type v} (toFun toFun_1 : α → Option β) (e_toFun : toFun = toFun_1) (invFun invFun_1 : β → Option α)
  (e_invFun : invFun = invFun_1) (inv : ∀ (a : α) (b : β), invFun b = some a ↔ toFun a = some b),
  { toFun := toFun, invFun := invFun, inv := inv } = { toFun := toFun_1, invFun := invFun_1, inv := ⋯ }
-- Mathlib.MeasureTheory.Function.EssSup
essInf_antitone_measure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f : α → β},
  μ.AbsolutelyContinuous ν →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae ν) f) essInf_antitone_measure._auto_1 →
      autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f)
          essInf_antitone_measure._auto_3 →
        essInf f ν ≤ essInf f μ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Lean.Elab.Command
Lean.Elab.Command.getRef : Lean.Elab.Command.CommandElabM Lean.Syntax