mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Basic
/-- Left inverse to a continuous map from a homeomorphism, mirroring `Equiv.symm_comp_self`.  -/
Homeomorph.symm_comp_toContinuousMap : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  (↑f.symm).comp ↑f = ContinuousMap.id α
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.directive : Lean.Elab.DocElabKind
-- Lean.Setup
Lean.instFromJsonModuleArtifacts : Lean.FromJson Lean.ModuleArtifacts
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.id_toFun' : ∀ (X : Pointed), (CategoryTheory.CategoryStruct.id X).toFun = id
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} [inst_3 : Inhabited (γ k)],
  m.WF → (Std.DHashMap.Raw.map f m).get! k = (Option.map (f k) (m.get? k)).get!
-- Init.Data.String.Basic
String.Pos.le_ofToSlice_iff : ∀ {s : String} {p : s.Pos} {q : s.toSlice.Pos}, p ≤ String.Pos.ofToSlice q ↔ p.toSlice ≤ q
-- Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
/-- The infinite product of strongly measurable functions is measurable, `HasProd` version.  -/
MeasureTheory.StronglyMeasurable.hasProd : ∀ {X : Type u_4} {E : Type u_5} {ι : Type u_6} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [ContinuousMul E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated]
  [TopologicalSpace.PseudoMetrizableSpace E] {f : ι → X → E} {g : X → E},
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
    (∀ (x : X), HasProd (fun i => f i x) (g x) L) → MeasureTheory.StronglyMeasurable g
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_biInter_finset : ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] (s : Finset ι) {f : ι → Set α},
  Bornology.IsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsCobounded (f i)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
ModuleCat.monoidalClosed_pre_app : ∀ {R : Type u} [inst : CommRing R] {M N : ModuleCat R} (P : ModuleCat R) (f : N ⟶ M),
  (CategoryTheory.MonoidalClosed.pre f).app P =
    ModuleCat.ofHom
      (↑ModuleCat.homLinearEquiv.symm ∘ₗ LinearMap.lcomp R (↑P) (ModuleCat.Hom.hom f) ∘ₗ ↑ModuleCat.homLinearEquiv)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.instSubsingletonQuotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  [Subsingleton M], Subsingleton (M ⧸ p)
-- Mathlib.Topology.Neighborhoods
Dense.open_subset_closure_inter : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, Dense s → IsOpen t → t ⊆ closure (t ∩ s)
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin_fun_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 ω₁ s x →
      DifferentiableWithinAt 𝕜 ω₂ s x →
        extDerivWithin (fun x => ω₁ x + ω₂ x) s x = extDerivWithin ω₁ s x + extDerivWithin ω₂ s x
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C],
  CategoryTheory.Limits.HasStrictInitialObjects C
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensRangeParams.mk.injEq : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier) (range : Lean.Lsp.Range)
  (textDocument_1 : Lean.Lsp.TextDocumentIdentifier) (range_1 : Lean.Lsp.Range),
  ({ textDocument := textDocument, range := range } = { textDocument := textDocument_1, range := range_1 }) =
    (textDocument = textDocument_1 ∧ range = range_1)
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Ioc_sdiff_Iic`. -/
Set.Ioc_diff_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a b \ Set.Iic c = Set.Ioc (max a c) b
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instSFiniteSndOfProd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} [MeasureTheory.SFinite ρ], MeasureTheory.SFinite ρ.snd
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.of_subtype_image : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {t : Set ↑s}, MeasurableSet (Subtype.val '' t) → MeasurableSet t
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.instInhabitedOfMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Mono f] → Inhabited (CategoryTheory.Limits.ImageFactorisation f)
-- Init.Data.SInt.Lemmas
Int32.toInt_div_of_ne_right : ∀ (a b : Int32), b ≠ -1 → (a / b).toInt = a.toInt.tdiv b.toInt
-- Std.Data.DTreeMap.Internal.Operations
/-- Changes the mapping of the key `k` by applying the function `f` to the current mapped value
(if any). This function can be used to insert a new mapping, modify an existing one or delete it.
This version of the function requires `LawfulEqOrd α`. There is an alternative non-dependent version
called `Const.alter`.
 -/
Std.DTreeMap.Internal.Impl.alter : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        (k : α) →
          (Option (β k) → Option (β k)) →
            (t : Std.DTreeMap.Internal.Impl α β) →
              t.Balanced → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (t.size - 1) (t.size + 1)
-- Init.Data.Nat.Lemmas
Nat.add_lt_add_of_le_of_lt : ∀ {a b c d : ℕ}, a ≤ b → c < d → a + c < b + d
-- Mathlib.Order.CompleteLattice.Basic
sInf_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sInf s = ⨅ a ∈ s, a
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.sup' : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] [inst_1 : SemilatticeSup M] {ι : Type u_3} {f : ι → α → M}
  (s : Finset ι),
  (∀ i ∈ s, Function.HasFiniteMulSupport (f i)) →
    ∀ (hs : s.Nonempty), Function.HasFiniteMulSupport fun a => s.sup' hs fun x => f x a
-- Mathlib.Data.Fin.Basic
Fin.sub_val_lt_sub : ∀ {n : ℕ} {i j : Fin n}, i ≤ j → ↑(j - i) < n - ↑i
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.congr : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜},
  HasGradientWithinAt f f' s x → (∀ x ∈ s, f₁ x = f x) → f₁ x = f x → HasGradientWithinAt f₁ f' s x
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.ofDiameter_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → EuclideanGeometry.Sphere.ofDiameter p₁ p₂ = s
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFrameAndPure_1 : ∀ {φ : Prop} (σs : List (Type u_1)) (P : Std.Do.SPred σs), Std.Do.SPred.Tactic.HasFrame spred(P ∧ ⌜φ⌝) P φ
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_X_some : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (x : S₁),
  (MvPolynomial.optionEquivLeft R S₁) (MvPolynomial.X (some x)) = Polynomial.C (MvPolynomial.X x)
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Checks if `val` is zero according to the ring tactic  -/
Mathlib.Tactic.Determinant.isZeroVal : {u : Lean.Level} →
  {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → {e : Q(«$α»)} → Mathlib.Tactic.Determinant.CertVal rα e → Bool
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.pushout.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f], CategoryTheory.Under.pushout f = CategoryTheory.Under.pushout f_1
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_mul : ∀ {w : ℕ} (x y : BitVec w) (i : ℕ), (x * y).getLsbD i = (x.mulRec y w).getLsbD i
-- Mathlib.Analysis.Convex.Function
concaveOn_iff_forall_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E}
  {f : E → β},
  ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.canonInst : Lean.Meta.Sym.Canon.ShouldCanonResult✝
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.Seq.omap.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option (α × β) → Sort u_3) (a : α) (b : β) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (b : β) → motive (some (a, b))),
  (match some (a, b) with
    | none => h_1 ()
    | some (a, b) => h_2 a b) =
    h_2 a b
-- Mathlib.Algebra.Lie.Abelian
LieModule.coe_maxTrivLinearMapEquivLieModuleHom : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (f : ↥(LieModule.maxTrivSubmodule R L (M →ₗ[R] N))),
  ⇑(LieModule.maxTrivLinearMapEquivLieModuleHom f) = ⇑↑f
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The `L^p` product of two isometries is an isometry.  -/
Isometry.withLpProdMap : ∀ (p : ENNReal) {α : Type u_2} {β : Type u_3} {α' : Type u_5} {β' : Type u_6} [hp : Fact (1 ≤ p)]
  [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] [inst_2 : PseudoEMetricSpace α']
  [inst_3 : PseudoEMetricSpace β'] {f : α → α'},
  Isometry f → ∀ {g : β → β'}, Isometry g → Isometry (WithLp.map p (Prod.map f g))
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle.injEq : ∀ (lhs : Bool) (s₁ s₂ : Lean.Grind.AC.Seq) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr)
  (lhs_1 : Bool) (s₁_1 s₂_1 : Lean.Grind.AC.Seq) (c₁_1 : Lean.Meta.Grind.AC.EqCnstr)
  (c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr),
  (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle lhs s₁ s₂ c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle lhs_1 s₁_1 s₂_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ s₁ = s₁_1 ∧ s₂ = s₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Init.SizeOf
Lean.Syntax.atom.sizeOf_spec : ∀ (info : Lean.SourceInfo) (val : String), sizeOf (Lean.Syntax.atom info val) = 1 + sizeOf info + sizeOf val
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- A category is an `InitialMonoClass` if the canonical morphism of an initial object is a
monomorphism.  In practice, this is most useful when given an arbitrary morphism out of the chosen
initial object, see `initial.mono_from`.
Given a terminal object, this is equivalent to the assumption that the unique morphism from initial
to terminal is a monomorphism, which is the second of Freyd's axioms for an AT category.

TODO: This is a condition satisfied by categories with zero objects and morphisms.
 -/
CategoryTheory.Limits.InitialMonoClass : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_neg : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelAddMonoid M] {f : ι → M}, f < 0 → ∑ i, f i < 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {f : β → β} {he : (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false},
  (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey he =
    if compare (t.minKey ⋯) k = Ordering.eq then k else t.minKey ⋯
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : FiberBundle F₁ E₁]
  [inst_14 : (x : B) → TopologicalSpace (E₂ x)] [inst_15 : FiberBundle F₂ E₂]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂]
  (p : Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x),
  ↑(Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂) p =
    (p.proj,
      (Bundle.Trivialization.continuousLinearMapAt 𝕜 e₂ p.proj).compContinuousAlternatingMap
        (p.snd.compContinuousLinearMap (Bundle.Trivialization.symmL 𝕜 e₁ p.proj)))
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.maxValueSealed_def : Int8.maxValueSealed✝ = Int8.maxValue
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_maxKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t → t.maxKey?.isSome = true
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.testFalseHelper : ∀ (p : ℕ),
  Nat.blt 1 p = true → Nat.ble 1 (LucasLehmer.norm_num_ext.sModNatTR (2 ^ p - 1) (p - 2)) = true → ¬LucasLehmerTest p
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} (aig : Std.Sat.AIG α) (idx : ℕ) (hidx : idx ≤ len)
  (s : aig.RefVec idx) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [inst_3 : Std.Sat.AIG.RefVec.LawfulMapOperator α f],
  Std.Sat.AIG.RefVec.map.go aig idx hidx s input f =
    if hidx : idx < len then
      let res := f aig (input.get idx hidx);
      let aig_1 := res.aig;
      have newRef := res.ref;
      have this := ⋯;
      have input_1 := input.cast this;
      have s := s.cast this;
      have s := s.push newRef;
      Std.Sat.AIG.RefVec.map.go aig_1 (idx + 1) ⋯ s input_1 f
    else
      have this := ⋯;
      { aig := aig, vec := this ▸ s }
-- Mathlib.Algebra.Ring.Defs
HasDistribNeg.mk : {α : Type u_1} →
  [inst : Mul α] →
    [toInvolutiveNeg : InvolutiveNeg α] →
      (∀ (x y : α), -x * y = -(x * y)) → (∀ (x y : α), x * -y = -(x * y)) → HasDistribNeg α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKey? k' = some k
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_inter_add_sdiff`. -/
MeasureTheory.measureReal_inter_add_diff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_inter_add_sdiff._auto_1 → μ.real (s ∩ t) + μ.real (s \ t) = μ.real s
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- Constructor for isomorphisms in the category `F.DescentData' sq sq₃`.  -/
CategoryTheory.Pseudofunctor.DescentData'.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  {D₁ D₂ : F.DescentData' sq sq₃} →
                    (e : (i : ι) → D₁.obj i ≅ D₂.obj i) →
                      autoParam
                          (∀ (i₁ i₂ : ι),
                            CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom)
                                (D₂.hom i₁ i₂) =
                              CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
                                ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom))
                          CategoryTheory.Pseudofunctor.DescentData'.isoMk._auto_1 →
                        (D₁ ≅ D₂)
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_mul_ball_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), {x} * Metric.ball 1 δ = Metric.ball x δ
-- Lean.Expr
/-- Similar to `etaExpanded?`, but only succeeds if `ₙ ≥ 1`.  -/
Lean.Expr.etaExpandedStrict? : Lean.Expr → Option Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.of_subsingleton : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α} [Subsingleton α], A.IsHermitian
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.mk.sizeOf_spec : ∀ (toGlueData : CategoryTheory.GlueData AlgebraicGeometry.LocallyRingedSpace)
  (f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (toGlueData.f i j)),
  sizeOf { toGlueData := toGlueData, f_open := f_open } = 1 + sizeOf toGlueData
-- Mathlib.Order.SuccPred.Basic
SuccOrder.ofCore.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (succ : α → α) (hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b)
  (hm : ∀ (a : α), IsMax a → succ a = a),
  SuccOrder.ofCore succ hn hm = { succ := succ, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Basic
/-- Pullback an `IsOrderedCancelMonoid` under a strictly monotone map.  -/
StrictMono.isOrderedCancelMonoid : ∀ {α : Type u} {β : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelMonoid α]
  [inst_3 : CommMonoid β] [inst_4 : LinearOrder β] (f : β → α),
  StrictMono f → (∀ (x y : β), f (x * y) = f x * f y) → IsOrderedCancelMonoid β
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.ofArray_eq_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (a : Array (α × β)),
  Std.DHashMap.Raw.Const.ofArray a = Std.DHashMap.Raw.Const.ofList a.toList
-- Init.Data.List.MapIdx
List.mapFinIdx_congr : ∀ {α : Type u_1} {β : Type u_2} {xs ys : List α} (w : xs = ys) (f : (i : ℕ) → α → i < xs.length → β),
  xs.mapFinIdx f = ys.mapFinIdx fun i a h => f i a ⋯
-- Mathlib.Order.UpperLower.Basic
isUpperSet_iInter₂ : ∀ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : LE α] {f : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), IsUpperSet (f i j)) → IsUpperSet (⋂ i, ⋂ j, f i j)
-- Mathlib.Algebra.CharP.Algebra
/-- If `R` has characteristic `p`, then so does `FractionRing R`.  -/
IsFractionRing.charP : ∀ (R : Type u_3) [inst : CommRing R] (p : ℕ) [IsDomain R] [CharP R p], CharP (FractionRing R) p
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.range_ofSubtype : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α),
  (alternatingGroup.ofSubtype s).range = Equiv.Perm.ofSubtype.range.subgroupOf (alternatingGroup α)
-- Mathlib.Analysis.Complex.IntegerCompl
Complex.add_intCast_mem_integerComplement : ∀ {x : ℂ} (a : ℤ), x + ↑a ∈ Complex.integerComplement ↔ x ∈ Complex.integerComplement
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSMul' : {β : Type u_2} → {α : Type u_1} → [SMul β α] → SMul (Colex β) α
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqExpr : BEq Nat.Internal.Linear.Expr
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.extend_zero : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁), F.extend 0 = f₀
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow_add_gt : ∀ {i j : ℕ}, j < i → ∀ (x : ℕ), (2 ^ i + x).testBit j = x.testBit j
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le : ∀ (𝕜 : Type u) {ι : Type v} (G : Type wG) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : Fintype ι] [inst_4 : Subsingleton ι] (i : ι),
  ‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖₊ ≤ 1
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.instIsAtomic : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] [inst_3 : OrderBot α], IsAtomic α
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_insert_sdiff_singleton : ∀ {α : Type u_1} (x : α) (s : Set α), s ⊆ insert x (s \ {x})
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.mul_const_le : ∀ {α : Type u_1} {b c : α} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α],
  b ≤ c → ∀ {a : α}, 0 ≤ a → a * b ≤ a * c
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₁ → (m₁ ∩ m₂).get? k = none
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- An absolute value as a monoid with zero homomorphism, assuming the target is a semifield.  -/
IsAbsoluteValue.abvHom' : {S : Type u_5} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      [IsCancelMulZero S] →
        {R : Type u_6} → [inst_3 : Semiring R] → [Nontrivial R] → (abv : R → S) → [IsAbsoluteValue abv] → R →*₀ S
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- `LinearMap.snd` as an isometry, when the first space has the zero quadratic form.  -/
QuadraticMap.Isometry.snd : {R : Type u_2} →
  (M₁ : Type u_3) →
    {M₂ : Type u_4} →
      {P : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R P] → (Q₂ : QuadraticMap R M₂ P) → QuadraticMap.prod 0 Q₂ →qᵢ Q₂
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
_private.Mathlib.AlgebraicTopology.DoldKan.Normalized.0.AlgebraicTopology.NormalizedMooreComplex.objX.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.ratLinear : ∀ {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive]
  [inst_5 : CategoryTheory.Linear ℚ C] [inst_6 : CategoryTheory.Linear ℚ D], CategoryTheory.Functor.Linear ℚ F
-- Mathlib.Algebra.Algebra.Prod
AlgEquiv.prodUnique_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Unique B] (x : A), AlgEquiv.prodUnique.symm x = (x, 0)
-- Aesop.Script.UScriptToSScript
_private.Aesop.Script.UScriptToSScript.0.Aesop.Script.StepTree.focusableGoals.go : {σ : Type} → Aesop.Script.StepTree → StateRefT' σ (Std.HashMap Lean.MVarId ℕ) (ST σ) (Array ℕ)