mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CategoryTheory.Functor.mapCochainComplexPlus.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : F.PreservesZeroMorphisms],
  F.mapCochainComplexPlus =
    (CochainComplex.plus D).lift ((CochainComplex.Plus.ι C).comp (F.mapHomologicalComplex (ComplexShape.up ℤ))) ⋯
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase_assoc : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.functor i)
      (CategoryTheory.CategoryStruct.comp d.toBase h) =
    CategoryTheory.CategoryStruct.comp (d.natTrans.app i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) h)
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.coe_of : ∀ (R : Type u) [inst : CommRing R] (X : Type v) [inst_1 : CommRing X] [inst_2 : HopfAlgebra R X],
  ↑{ X := X, commRing := inst_1, hopfAlgebra := inst_2 } = X
-- Lean.Meta.Sym.Arith.Poly
/-- Monomial factor applied to polynomial `p₁`.  -/
Lean.Grind.CommRing.SPolResult.m₁ : Lean.Grind.CommRing.SPolResult → Lean.Grind.CommRing.Mon
-- Lean.DocString.Types
Lean.Doc.instInhabitedPart : {a : Type u_1} → {a_1 : Type u_2} → {a_2 : Type u_3} → Inhabited (Lean.Doc.Part a a_1 a_2)
-- Mathlib.Logic.Function.Basic
Function.Injective.isPartialInv : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β}, Function.Injective f → Function.IsPartialInv f (Function.partialInv f)
-- Mathlib.LinearAlgebra.Transvection.Basic
IsBaseChange.transvection : ∀ {R : Type u_3} {V : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (A : Type u_5)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {W : Type u_6} [inst_5 : AddCommMonoid W] [inst_6 : Module R W]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {ε : V →ₗ[R] W} (ibc : IsBaseChange A ε) (f : Module.Dual R V)
  (v : V), ibc.endHom (LinearMap.transvection f v) = LinearMap.transvection (ibc.toDual f) (ε v)
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `FunLike.coe_zero`. -/
Seminorm.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_sub : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Ring R] [inst_1 : Ring S] (f : R →+ S)
  (x y : AddMonoidAlgebra R M), AddMonoidAlgebra.map f (x - y) = AddMonoidAlgebra.map f x - AddMonoidAlgebra.map f y
-- Mathlib.Algebra.Category.Ring.Instances
localization_unit_isIso' : ∀ (R : CommRingCat), CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))
-- Mathlib.Algebra.Algebra.Rat
Rat.instSMulCommClass' : ∀ {R : Type u_2} {S : Type u_3} [inst : DivisionRing S] [inst_1 : CharZero S] [inst_2 : SMul R S] [SMulCommClass S R S],
  SMulCommClass R ℚ S
-- Mathlib.Condensed.TopCatAdjunction
/-- Let `X` be a condensed set. We define a topology on `X(*)` as the quotient topology of
all the maps from compact Hausdorff `S` spaces to `X(*)`, corresponding to elements of `X(S)`.
In other words, the topology coinduced by the map `CondensedSet.coinducingCoprod` above.  -/
instTopologicalSpaceObjOppositeCompHausObjFunctorTypeIsSheafCoherentTopologyOpOfPUnit : (X : CondensedSet) → TopologicalSpace (X.obj.obj (Opposite.op (CompHaus.of PUnit.{u + 1})))
-- Init.Data.UInt.Bitwise
UInt8.ofNat_xor : ∀ (a b : ℕ), UInt8.ofNat (a ^^^ b) = UInt8.ofNat a ^^^ UInt8.ofNat b
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₇_isSymm : CartanMatrix.E₇.IsSymm
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The singleton operation as a `OneHom`.  -/
Finset.singletonOneHom : {α : Type u_2} → [inst : One α] → OneHom α (Finset α)
-- Batteries.Data.Array.Basic
Array.scanrM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m β) (init : β) (as : Array α)
  (start stop : ℕ) (h_start : start ≤ as.size) (acc : Array β),
  Array.scanrM.loop f init as start stop h_start acc =
    if h_gt : stop < start then
      let i := start - 1;
      do
      let next ← f as[i] init
      Array.scanrM.loop f next as i stop ⋯ (acc.push init)
    else pure (acc.push init).reverse
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_sub`. -/
ENat.coe_sub : ∀ (m n : ℕ), ↑(m - n) = ↑m - ↑n
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.orderIsoRpow_symm_eq : ∀ (y : ℝ) (hy : 0 < y), (NNReal.orderIsoRpow y hy).symm = NNReal.orderIsoRpow (1 / y) ⋯
-- Mathlib.LinearAlgebra.InvariantBasisNumber
InvariantBasisNumber.mk : ∀ {R : Type u} [inst : Semiring R], (∀ {n m : ℕ} (a : (Fin n → R) ≃ₗ[R] Fin m → R), n = m) → InvariantBasisNumber R
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.additive_yonedaObj' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : C),
  (CategoryTheory.preadditiveYoneda.obj X).Additive
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
_private.Mathlib.LinearAlgebra.Matrix.FixedDetMatrices.0.FixedDetMatrices.prop_red_S : ∀ {m : ℤ} {C : FixedDetMatrix (Fin 2) ℤ m → Prop},
  (∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.S • B)) →
    ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C (ModularGroup.S • B) ↔ C B
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_sub : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Sub β] (f g : α → β),
  (UniformOnFun.ofFun 𝔖) (f - g) = (UniformOnFun.ofFun 𝔖) f - (UniformOnFun.ofFun 𝔖) g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insert!_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert! k v t).size ≤ t.size + 1
-- Mathlib.Algebra.BigOperators.Finprod
finprod_congr_Prop : ∀ {M : Type u_2} [inst : CommMonoid M] {p q : Prop} {f : p → M} {g : q → M} (hpq : p = q),
  (∀ (h : q), f ⋯ = g h) → finprod f = finprod g
-- Init.Data.Range.Polymorphic.PRange
Std.Roc.mk : {α : Type u} → α → α → Std.Roc α
-- Mathlib.Tactic.Linarith.Frontend
/-- Allow elaboration of `LinarithConfig` arguments to tactics.
 -/
Mathlib.Tactic.elabLinarithConfig : Lean.Syntax →
  optParam Mathlib.Tactic.Linarith.LinarithConfig { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Tactic.Linarith.LinarithConfig
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `IsCancelMul` across an `Equiv`  -/
Equiv.isCancelMul : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Mul β] [IsCancelMul β], IsCancelMul α
-- Mathlib.Data.Set.Insert
Set.insert_eq_of_mem : ∀ {α : Type u_1} {a : α} {s : Set α}, a ∈ s → insert a s = s
-- Mathlib.Data.Set.Order
/-- **Alias** of `Set.antitone_ofPred`. -/
Set.antitone_setOf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {p : α → β → Prop},
  (∀ (b : β), Antitone fun a => p a b) → Antitone fun a => {b | p a b}
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.F₄.eq_1 : CartanMatrix.F₄ = !![2, -1, 0, 0; -1, 2, -2, 0; 0, -1, 2, -1; 0, 0, -1, 2]
-- Mathlib.Data.Set.Image
Set.range_nonempty_iff_nonempty : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α}, (Set.range f).Nonempty ↔ Nonempty ι
-- Mathlib.Data.List.Chain
/-- Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
the predicate is true everywhere in the chain and at `a`.
That is, we can propagate the predicate up the chain.
 -/
List.IsChain.backwards_induction : ∀ {α : Type u_1} {r : α → α → Prop} (p : α → Prop) (l : List α),
  List.IsChain r l → (∀ ⦃x y : α⦄, r x y → p y → p x) → (∀ (lne : l ≠ []), p (l.getLast lne)) → ∀ i ∈ l, p i
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The step function for the TM2 model.  -/
Turing.TM2.step : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        [DecidableEq K] → (Λ → Turing.TM2.Stmt Γ Λ σ) → Turing.TM2.Cfg Γ Λ σ → Option (Turing.TM2.Cfg Γ Λ σ)
-- Mathlib.Data.Seq.Computation
Computation.terminates_congr : ∀ {α : Type u} {c₁ c₂ : Computation α}, c₁.Equiv c₂ → (c₁.Terminates ↔ c₂.Terminates)
-- Std.Tactic.Do.Syntax
/-- If `false` (the default), then we aggressively split `if` and `match` statements and inline join
points unconditionally. For some programs this causes exponential blowup of VCs.
Set this flag to choose a more conservative (but slightly lossy) encoding that traverses
every join point only once and yields a formula the size of which is linear in the number of
control flow splits.
 -/
Lean.Elab.Tactic.Do.VCGen.Config.jp : Lean.Elab.Tactic.Do.VCGen.Config → Bool
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.derivative_rootMultiplicity_of_root : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R},
  p.IsRoot t → Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1
-- Mathlib.Topology.Connected.Basic
isConnected_singleton : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsConnected {x}
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_inter_compl_left_subset : ∀ {α : Type u_1} (s t : Set α), (s ∪ t) ∩ sᶜ ⊆ t
-- Mathlib.RingTheory.AlgebraTower
/-- A natural number that is invertible when coerced to `R` is also invertible
when coerced to any `R`-algebra.  -/
IsScalarTower.invertibleAlgebraCoeNat : (R : Type u_1) →
  (A : Type u_3) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → (n : ℕ) → [inv : Invertible ↑n] → Invertible ↑n
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableAt.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {f : E → E},
  DifferentiableAt 𝕜 f x → f x = x → ∀ (n : ℕ), DifferentiableAt 𝕜 f^[n] x
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
HasFDerivAt.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {f' : E →L[𝕜'] F}
  {x : E}, HasFDerivAt f f' x → HasFDerivAt f (ContinuousLinearMap.restrictScalars 𝕜 f') x
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.Hom.eq_2 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (x_2 y : D), (CategoryTheory.Join.right x_2).Hom (CategoryTheory.Join.right y) = ULift.{v₁, v₂} (x_2 ⟶ y)
-- Mathlib.Topology.Constructions
ULift.topologicalSpace : {X : Type u} → [t : TopologicalSpace X] → TopologicalSpace (ULift.{v, u} X)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_one_of_forall_eq_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M}, (∀ (x : α), f x = 1) → ∏ᶠ (i : α), f i = 1
-- Mathlib.GroupTheory.IsSubnormal
/-- **Alias** of the forward direction of `Subgroup.IsSubnormal.isSubnormal_iff`.

---

A characterisation of satisfying `IsSubnormal` in terms of chains of subgroups, each normal in
the following one.

The sequence stabilises once it reaches `⊤`, which is guaranteed at the asserted `n`.
 -/
Subgroup.IsSubnormal.exists_chain : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  H.IsSubnormal → ∃ n f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- A type class witnessing the fact that `R₀` contains enough coefficients to descend
`P` to a submersive presentation.  -/
Algebra.SubmersivePresentation.HasCoeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                Algebra.SubmersivePresentation R S ι σ →
                  (R₀ : Type u_5) →
                    [inst_4 : CommRing R₀] →
                      [inst_5 : Algebra R₀ R] → [inst_6 : Algebra R₀ S] → [IsScalarTower R₀ R S] → Prop
-- Init.Data.String.Basic
String.Slice.copy_eq_copy_sliceTo : ∀ {s : String.Slice} {pos : s.Pos}, s.copy = (s.sliceTo pos).copy ++ (s.sliceFrom pos).copy
-- Mathlib.Order.Filter.AtTopBot.Archimedean
tendsto_natCast_atTop_atTop : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R],
  Filter.Tendsto Nat.cast Filter.atTop Filter.atTop
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
hasMFDerivWithinAt_iff_hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E} {x : E}
  {f' : TangentSpace (modelWithCornersSelf 𝕜 E) x →L[𝕜] TangentSpace (modelWithCornersSelf 𝕜 E') (f x)},
  HasMFDerivAt[s] f x f' ↔ HasFDerivWithinAt f f' s x
-- Init.Data.String.OrderInstances
String.Internal.tacticOrder : Lean.ParserDescr
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.equiv_iff_toArray_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ ↔ t₁.toArray.Perm t₂.toArray
-- Mathlib.Algebra.Group.Equiv.Defs
/-- An alias for `h.symm.map_mul`. Introduced to fix the issue in
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth
 -/
MulEquiv.symm_map_mul : ∀ {M : Type u_9} {N : Type u_10} [inst : Mul M] [inst_1 : Mul N] (h : M ≃* N) (x y : N),
  h.symm (x * y) = h.symm x * h.symm y
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.LocallyQuasiFinite.of_finite_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f],
  (∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite) → AlgebraicGeometry.LocallyQuasiFinite f
-- Init.Data.UInt.Lemmas
UInt32.ofNatTruncate_finVal : ∀ (n : Fin UInt32.size), UInt32.ofNatClamp ↑n = UInt32.ofFin n
-- Mathlib.Data.ENNReal.Inv
ENNReal.zpow_le_one_of_nonpos : ∀ {n : ℤ}, n ≤ 0 → ∀ {x : ENNReal}, 1 ≤ x → x ^ n ≤ 1
-- Mathlib.Data.List.Basic
List.filterMap_eq_flatMap_toList : ∀ {α : Type u} {β : Type v} (f : α → Option β) (l : List α), List.filterMap f l = List.flatMap (fun a => (f a).toList) l
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.center.eq_1 : ∀ (G : Type u_1) [inst : Group G], Subgroup.center G = { toSubmonoid := Submonoid.center G, inv_mem' := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a fallback : α} {v : β k},
  (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableAt.mul` -/
DifferentiableAt.fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸},
  DifferentiableAt 𝕜 a x → DifferentiableAt 𝕜 b x → DifferentiableAt 𝕜 (fun i => a i * b i) x
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.derivWithin_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → derivWithin f₁ s x = derivWithin f s x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.elseBranch : Lean.Elab.Term.Do.DoIfView → Lean.Syntax
-- Mathlib.Topology.UniformSpace.Ultra.Basic
ball_eq_of_mem : ∀ {X : Type u_1} {V : SetRel X X} [V.IsSymm] [V.IsTrans] {x y : X},
  y ∈ UniformSpace.ball x V → UniformSpace.ball x V = UniformSpace.ball y V
-- Init.Data.String.Iterate
String.Slice.RevPosIterator : String.Slice → Type
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.eq_1 : ∀ (M : Type u_1) {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] (K : ℝ) (A B : Set X),
  CovByVAdd M K A B = ∃ F, ↑F.card ≤ K ∧ A ⊆ ↑F +ᵥ B
-- ProofWidgets.Data.Html
ProofWidgets.Html.brecOn_1.eq : ∀ {motive_1 : ProofWidgets.Html → Sort u} {motive_2 : Array ProofWidgets.Html → Sort u}
  {motive_3 : List ProofWidgets.Html → Sort u} (t : Array ProofWidgets.Html)
  (F_1 : (t : ProofWidgets.Html) → t.below → motive_1 t)
  (F_2 : (t : Array ProofWidgets.Html) → ProofWidgets.Html.below_1 t → motive_2 t)
  (F_3 : (t : List ProofWidgets.Html) → ProofWidgets.Html.below_2 t → motive_3 t),
  ProofWidgets.Html.brecOn_1 t F_1 F_2 F_3 = F_2 t (ProofWidgets.Html.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_one : ∀ {R : Type u_2} {a b : R} [inst : CommRing R], QuadraticAlgebra.norm 1 = 1
-- Std.Time.Format.Modifier
Std.Time.Modifier.q.inj : ∀ {presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text},
  Std.Time.Modifier.q presentation = Std.Time.Modifier.q presentation_1 → presentation = presentation_1
-- Init.Data.String.Iterate
String.Slice.instInhabitedPosIterator : {a : String.Slice} → Inhabited a.PosIterator
-- Init.Data.UInt.Lemmas
UInt16.lt_of_lt_of_le : ∀ {a b c : UInt16}, a < b → b ≤ c → a < c
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The vector from the midpoint of a chord to the center of the sphere is
orthogonal to the chord.  -/
EuclideanGeometry.Sphere.inner_vsub_center_midpoint_vsub : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P} {s : EuclideanGeometry.Sphere P},
  p₁ ∈ s → p₂ ∈ s → inner ℝ (s.center -ᵥ midpoint ℝ p₁ p₂) (p₂ -ᵥ p₁) = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_pi : Real.tan Real.pi = 0
-- Mathlib.Order.SuccPred.LinearLocallyFinite
countable_of_linear_succ_pred_arch : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [PredOrder ι] [IsSuccArchimedean ι], Countable ι
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_smul_left : ∀ {𝕜 : Type u_2} {F : Type u_7} {ι : Type u_9} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup F]
  [inst_2 : Module 𝕜 F] (p : SeminormFamily 𝕜 F ι) (x : 𝕜),
  ∀ U ∈ p.basisSets, ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' U
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_inter' : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω},
  s.Finite →
    (ProbabilityTheory.uniformOn s) (t ∩ u) =
      (ProbabilityTheory.uniformOn (s ∩ u)) t * (ProbabilityTheory.uniformOn s) u
-- Init.Data.SInt.Bitwise
Int8.toUInt8_or : ∀ (a b : Int8), (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
-- Init.PropLemmas
Bool.dite_else_true_eq_false : ∀ {p : Prop} [inst : Decidable p] {x : p → Bool}, (if h : p then x h else true) = false ↔ ∃ (h : p), x h = false
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A list with product less than one must have positive length.  -/
List.length_pos_of_prod_lt_one : ∀ {M : Type u_4} [inst : Monoid M] [inst_1 : Preorder M] (L : List M), L.prod < 1 → 0 < L.length
-- Mathlib.CategoryTheory.EssentialImage
/-- The essential image of a functor `F` consists of those objects in the target category which are
isomorphic to an object in the image of the function `F.obj`. In other words, this is the closure
under isomorphism of the function `F.obj`.
This is the "non-evil" way of describing the image of a functor.
 -/
CategoryTheory.Functor.essImage : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty D
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.Pi.empty.congr_simp : ∀ {α : Type u_1} (β : α → Sort u_2) (a : α) (h : a ∈ ∅), Finset.Pi.empty β a h = Finset.Pi.empty β a h
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : SizeOf C] (X : C) [comon : CategoryTheory.ComonObj X],
  sizeOf { X := X, comon := comon } = 1 + sizeOf X + sizeOf comon
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.add_norm_nonneg : ∀ {α : Type u_1} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ),
  0 ≤ f + BoundedContinuousFunction.const α ‖f‖
-- Mathlib.Data.Finsupp.Basic
Finsupp.graph_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M], Finsupp.graph 0 = ∅
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.sheafedSpaceObj_carrier : ∀ (R : CommRingCat), ↑(AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace = AlgebraicGeometry.Spec.topObj R
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.finite_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, s⁻¹.Finite ↔ s.Finite
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_eq_norm_coeFn : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) [inst_3 : Fintype α], ‖f‖ = ‖⇑f‖
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.mulRingSeminormClass : ∀ {R : Type u_1} [inst : NonAssocRing R], MulRingSeminormClass (MulRingSeminorm R) R ℝ
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
/-- The functorial (distinguished) triangles that are part of the spectral
object attached to objects in a triangulated category equipped with a t-structure.  -/
CategoryTheory.Triangulated.TStructure.triangleω₁δ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C →
                [CategoryTheory.IsTriangulated C] →
                  (a b c : EInt) → a ≤ b → b ≤ c → CategoryTheory.Functor C (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.RingTheory.AdjoinRoot
/-- `algEquivOfAssociated` sends `AdjoinRoot.root f` to `AdjoinRoot.root g`.  -/
AdjoinRoot.algEquivOfAssociated_root : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hfg : Associated f g), (AdjoinRoot.algEquivOfAssociated R f g hfg) (AdjoinRoot.root f) = AdjoinRoot.root g
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.subsingleton_iffₛ : ∀ {R : Type u} [inst : CommSemiring R],
  Subsingleton (CommRing.Pic R) ↔
    ∀ (M : Type u) [inst_1 : AddCommMonoid M] [inst_2 : Module R M], Module.Invertible R M → Module.Free R M
-- Std.Time.Date.PlainDate
_private.Std.Time.Date.PlainDate.0.Std.Time.PlainDate.localizedDayOfWeek : Std.Time.Weekday → Std.Time.Weekday → Std.Time.Internal.Bounded.LE 0 6
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey?_modify_eq_maxKey? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).maxKey? = t.maxKey?