mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j) =
    CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.pushHex.match_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  n = 0 →
    (match n with
      | 0 => h_1 ()
      | k.succ => h_2 k) ≍
      h_1 ()
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Bounded.eq_3 : ∀ {α : Type u_1} [inst : Preorder α] (x : WithBot α) (x_1 : WithTop α) (size : ℕ) (l : Ordnode α) (x_3 : α)
  (r : Ordnode α), (Ordnode.node size l x_3 r).Bounded x x_1 = (l.Bounded x ↑x_3 ∧ r.Bounded (↑x_3) x_1)
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- A surjective group homomorphism `φ : G →* H` with `N = ker(φ)` descends (i.e. `lift`s) to a
group isomorphism `G/N ≃* H`.  -/
QuotientGroup.liftEquiv : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Group G] →
      [inst_1 : Group H] →
        (N : Subgroup G) → [nN : N.Normal] → {φ : G →* H} → Function.Surjective ⇑φ → N = φ.ker → G ⧸ N ≃* H
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_iInf : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {ι : Sort u_5} [Nonempty ι] (f : F),
  Function.Injective ⇑f → ∀ (s : ι → Submonoid M), Submonoid.map f (iInf s) = ⨅ i, Submonoid.map f (s i)
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.isLocal_affineProperty : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : outParam AlgebraicGeometry.AffineTargetMorphismProperty} [self : AlgebraicGeometry.HasAffineProperty P Q],
  Q.IsLocal
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsIntegralInt : ∀ {K : Type u_1} [inst : Field K], Algebra.IsIntegral ℤ (NumberField.RingOfIntegers K)
-- Mathlib.GroupTheory.Finiteness
/-- The product of two finitely generated groups is finitely generated.  -/
Prod.instGroupFG : ∀ {G : Type u_3} [inst : Group G] {G' : Type u_5} [inst_1 : Group G'] [Group.FG G] [Group.FG G'], Group.FG (G × G')
-- Mathlib.Analysis.SumIntegralComparisons
/-- **Integral test**: bounds the sum from 1 by an integral.  -/
AntitoneOn.tsum_add_one_le_integral : ∀ {f : ℝ → ℝ},
  AntitoneOn f (Set.Ici 0) →
    MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
      (∀ t ∈ Set.Ioi 0, 0 ≤ f t) → ∑' (n : ℕ), f ↑(n + 1) ≤ ∫ (x : ℝ) in Set.Ioi 0, f x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.instIsLeftAdjointFunctorColim : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.colim.IsLeftAdjoint
-- Init.Data.Repr
instReprListOfReprAtom : {α : Type u_1} → [Repr α] → [ReprAtom α] → Repr (List α)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integralCLM'_L1_eq_integral : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : NormedAddCommGroup E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E]
  [inst_4 : IsBoundedSMul 𝕜 E] [inst_5 : SMulCommClass ℝ 𝕜 E] [inst_6 : CompleteSpace E] (f : ↥(α →₁ₛ[μ] E)),
  (MeasureTheory.L1.integralCLM' 𝕜) ↑f = MeasureTheory.L1.SimpleFunc.integral f
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ}
  (refs refs_1 : Vector Std.Sat.AIG.Fanin w) (e_refs : refs = refs_1)
  (hrefs : ∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size),
  { refs := refs, hrefs := hrefs } = { refs := refs_1, hrefs := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.ofNatLT_zero : ∀ {w : ℕ} {h : 0 < 2 ^ w}, 0#'h = 0#w
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_vaddConst' : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (p : P),
  ⇑(AffineEquiv.vaddConst 𝕜 p) = fun v => v +ᵥ p
-- Mathlib.Algebra.FreeAlgebra
_private.Mathlib.Algebra.FreeAlgebra.0.FreeAlgebra.mk_mul : ∀ (R : Type u_1) (X : Type u_2) [inst : CommSemiring R] (x y : FreeAlgebra.Pre R X),
  Quot.mk (FreeAlgebra.Rel R X) (x * y) = Quot.mk (FreeAlgebra.Rel R X) x * Quot.mk (FreeAlgebra.Rel R X) y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {h' : a ∈ t.erase k}, Std.DTreeMap.Const.get (t.erase k) a h' = Std.DTreeMap.Const.get t a ⋯
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.multSum_eq_main_err : ∀ {s : BoundingSieve} (d : ℕ), BoundingSieve.multSum d = s.nu d * s.totalMass + BoundingSieve.rem d
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- For complex-valued `f`, establish a simple relation between the proximity functions of `f` and of
`f⁻¹`.
 -/
ValueDistribution.proximity_inv : ∀ {f : ℂ → ℂ}, ValueDistribution.proximity f⁻¹ ⊤ = ValueDistribution.proximity f 0
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.inv_def : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Inv (G i)] (f : (i : ι) → G i), f⁻¹ = fun i => (f i)⁻¹
-- Lean.Parser.Command
/-- Syntax quotation for (sequences of) commands.
The identical syntax for term quotations takes priority,
so ambiguous quotations like `` `($x $y) `` will be parsed as an application,
not two commands. Use `` `($x:command $y:command) `` instead.
Multiple commands will be put in a `` `null `` node,
but a single command will not (so that you can directly
match against a quotation in a command kind's elaborator).  -/
Lean.Parser.Command.quot : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.instSubsingletonIsPointwiseRightKanExtensionAt : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) (Y : D),
  Subsingleton (E.IsPointwiseRightKanExtensionAt Y)
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.decodeSum.match_1.splitter : (motive : Bool → ℕ → Sort u_1) →
  (x : Bool) →
    (x_1 : ℕ) → ((m : ℕ) → motive false m) → ((x : Bool) → (m : ℕ) → (x = false → False) → motive x m) → motive x x_1
-- Init.Data.Range.Polymorphic.UInt
UInt64.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite UInt64
-- Batteries.Util.ProofWanted
DerivedWanted.ofVal.injEq : ∀ {α : Sort u} (val val_1 : α), ({ val := val } = { val := val_1 }) = (val = val_1)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.triangle : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor B C),
  CategoryTheory.CategoryStruct.comp (F.associator (CategoryTheory.Functor.id B) G).hom
      (F.whiskerLeft G.leftUnitor.hom) =
    CategoryTheory.Functor.whiskerRight F.rightUnitor.hom G
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_one : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MulArchimedeanClass.mk 1 = ⊤
-- Mathlib.LinearAlgebra.Eigenspace.Semisimple
/-- A semisimple endomorphism is triangularizable if and only if it is diagonalizable.  -/
Module.End.IsSemisimple.iSup_maxGenEigenspace_eq_top_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, f.IsSemisimple → (⨆ μ, f.maxGenEigenspace μ = ⊤ ↔ ⨆ μ, f.eigenspace μ = ⊤)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
/-- Define a left action of `C` on `D` from a right action of `Cᴹᵒᵖ` on `D` via
the formula `c ⊙ₗ d := d ⊙ᵣ (mop c)`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory.MonoidalRightAction Cᴹᵒᵖ D] →
            CategoryTheory.MonoidalCategory.MonoidalLeftAction C D
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.card_iUnion_lt_iff_forall_of_isRegular : ∀ {c : Cardinal.{u}} {ι α : Type u} {t : ι → Set α},
  c.IsRegular → Cardinal.mk ι < c → (Cardinal.mk ↑(⋃ i, t i) < c ↔ ∀ (i : ι), Cardinal.mk ↑(t i) < c)
-- Mathlib.Analysis.Normed.Module.Extr
/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum on a set `s` at a point `c`,
then the function `fun x => ‖f x + f c‖` has a maximum on `s` at `c`.  -/
IsMaxOn.norm_add_self : ∀ {α : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} {s : Set α} {c : α},
  IsMaxOn (norm ∘ f) s c → IsMaxOn (fun x => ‖f x + f c‖) s c
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.instOrderTopPrimeSpectrum : (R : Type u) → [inst : CommSemiring R] → [IsLocalRing R] → OrderTop (PrimeSpectrum R)
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefKind.defWanted.sizeOf_spec : sizeOf WantedRefKind.defWanted✝ = 1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_rpow : ∀ {y : ℝ}, y ≠ 0 → ∀ (x : NNReal), (x ^ y⁻¹) ^ y = x
-- Init.Data.SInt.Bitwise
Int64.shiftRight_xor : ∀ {a b c : Int64}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Init.Data.Format.Basic
/-- The default indentation level, which is two spaces.  -/
Std.Format.defIndent : ℕ
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_le_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v.restrict x ≤ v.restrict y ↔ v x ≤ v y
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Abundant.pos : ∀ {n : ℕ}, n.Abundant → 0 < n
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.indepFun_const_right : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
  [ProbabilityTheory.IsZeroOrMarkovKernel κ] (X : Ω → β) (c : β'), ProbabilityTheory.Kernel.IndepFun X (fun x => c) κ μ
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.instEquivLike.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N],
  MulEquiv.instEquivLike =
    { coe := fun f => f.toFun, inv := fun f => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_two : Squarefree 2
-- Std.Data.TreeMap.Raw.Lemmas
/-- Variant of `getElem!_map` that holds without `LawfulEqCmp`.  -/
Std.TreeMap.Raw.getElem!_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → γ} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.map f t)[k]! = (Option.pmap (fun v h => f (t.getKey k h) v) t[k]? ⋯).get!
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integral_neg : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.integral I l (-f) vol = -BoxIntegral.integral I l f vol
-- Mathlib.Algebra.Algebra.Basic
Algebra.algebraMapSubmonoid_powers : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Algebra R S] (r : R),
  Algebra.algebraMapSubmonoid S (Submonoid.powers r) = Submonoid.powers ((algebraMap R S) r)
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigits_nonneg : ∀ {b : ℕ} (digits : ℕ → Fin b), 0 ≤ Real.ofDigits digits
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.str.sizeOf_spec : ∀ (val : String), sizeOf (Lean.Compiler.LCNF.LitValue.str val) = 1 + sizeOf val
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonStaticRegistrationOptions.fromJson : Lean.Json → Except String Lean.Lsp.StaticRegistrationOptions
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.map_section_ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f : X ⟶ Y} (se : CategoryTheory.SplitEpi f) (F : CategoryTheory.Functor C D),
  (se.map F).section_ = F.map se.section_
-- Mathlib.Analysis.Calculus.Deriv.Basic
DifferentiableOn.hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  DifferentiableOn 𝕜 f s → s ∈ nhds x → HasDerivAt f (deriv f x) x
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_lt_omega0 : ∀ {a : Cardinal.{u_1}}, a.ord < Ordinal.omega0 ↔ a < Cardinal.aleph0
-- Mathlib.Algebra.GroupWithZero.Semiconj
Commute.zpow_zpow_self₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (m n : ℤ), Commute (a ^ m) (a ^ n)
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.normedAddGroup : {E : Type u_2} → [NormedAddGroup E] → NormedAddGroup (ULift.{u_5, u_2} E)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- For `x ≤ 0` the defining sum diverges, so the kernel is 0.  -/
HurwitzZeta.evenKernel_undef : ∀ (a : UnitAddCircle) {x : ℝ}, x ≤ 0 → HurwitzZeta.evenKernel a x = 0
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_def : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
  m.sPolynomial f g =
    (MvPolynomial.monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f -
      (MvPolynomial.monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_empty : ∀ {α : Type u_1} [inst : Preorder α], ∅.OrdConnected
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
ModuleCat.ihom_map_apply : ∀ {R : Type u} [inst : CommRing R] {M N P : ModuleCat R} (f : N ⟶ P) (g : ↑(ModuleCat.of R (M ⟶ N))),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.ihom M).map f)) g = CategoryTheory.CategoryStruct.comp g f
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toEquiv_pointReflection : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (x : P₁), (AffineEquiv.pointReflection k x).toEquiv = Equiv.pointReflection x
-- Mathlib.AlgebraicGeometry.Restrict
/-- Restricting a morphism twice onto a basic open set is isomorphic to one restriction.  -/
AlgebraicGeometry.morphismRestrictRestrictBasicOpen : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (U : Y.Opens) →
      (r : ↑(Y.presheaf.obj (Opposite.op U))) →
        CategoryTheory.Arrow.mk
            (f ∣_ U ∣_
              (↑U).basicOpen ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op)) r)) ≅
          CategoryTheory.Arrow.mk (f ∣_ Y.basicOpen r)
-- Init.Meta.Defs
/-- Finds the tail position of the trailing whitespace of the first `SourceInfo` from the back of `stx`.
If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
no trailing whitespace and lacks a tail position, the result is `none`.
 -/
Lean.Syntax.getTrailingTailPos? : Lean.Syntax → optParam Bool false → Option String.Pos.Raw
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.finrank_of_bijective_toSpanSingleton : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {x : M}, Function.Bijective ⇑(LinearMap.toSpanSingleton R M x) → Module.finrank R M = 1
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `indiscreteTopology_iff_forall_nnnorm_eq_zero'`. -/
IndiscreteTopology.of_forall_nnnorm_eq_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E], (∀ (x : E), ‖x‖₊ = 0) → IndiscreteTopology E
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.add_compat_right : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X a b → FreeAlgebra.Rel R X (c + a) (c + b)
-- Mathlib.Data.FunLike.Equiv
EquivLike.inv_apply_eq : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] {e : E} {b : β} {a : α},
  EquivLike.inv e b = a ↔ b = e a
-- Aesop.Forward.State
Aesop.Hyp.mk.inj : ∀ {fvarId? : Option Lean.FVarId} {subst : Aesop.Substitution} {fvarId?_1 : Option Lean.FVarId}
  {subst_1 : Aesop.Substitution},
  { fvarId? := fvarId?, subst := subst } = { fvarId? := fvarId?_1, subst := subst_1 } →
    fvarId? = fvarId?_1 ∧ subst = subst_1
-- Mathlib.Data.Stream.Defs
/-- The stream of natural numbers: `Stream'.get n Stream'.nats = n`.  -/
Stream'.nats : Stream' ℕ
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.mapToSubgraph.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (x : G.Walk u v),
  x.mapToSubgraph =
    match v, x with
    | .(u), SimpleGraph.Walk.nil => SimpleGraph.Walk.nil
    | v, SimpleGraph.Walk.cons h p =>
      have h_1 := ⋯;
      have h_2 := h_1;
      SimpleGraph.Walk.cons h_2 (SimpleGraph.Walk.map (SimpleGraph.Subgraph.inclusion ⋯) p.mapToSubgraph)
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.TreeMap.Raw.getKeyLED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α → α
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Sequence of partial numerator and denominator pairs.  -/
GenContFract.s : {α : Type u_1} → GenContFract α → Stream'.Seq (GenContFract.Pair α)
-- Mathlib.Topology.VectorBundle.Basic
/-- Rewrite `ContinuousLinearMap.inCoordinates` in a `VectorBundleCore`.  -/
VectorBundleCore.inCoordinates_eq : ∀ {B : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : TopologicalSpace B] {𝕜₁ : Type u_5}
  {𝕜₂ : Type u_6} [inst_2 : NontriviallyNormedField 𝕜₁] [inst_3 : NontriviallyNormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
  {B' : Type u_7} [inst_4 : TopologicalSpace B'] [inst_5 : NormedSpace 𝕜₁ F] {F' : Type u_8}
  [inst_6 : NormedAddCommGroup F'] [inst_7 : NormedSpace 𝕜₂ F'] {ι : Type u_10} {ι' : Type u_11}
  (Z : VectorBundleCore 𝕜₁ B F ι) (Z' : VectorBundleCore 𝕜₂ B' F' ι') {x₀ x : B} {y₀ y : B'} (ϕ : F →SL[σ] F'),
  x ∈ Z.baseSet (Z.indexAt x₀) →
    y ∈ Z'.baseSet (Z'.indexAt y₀) →
      ContinuousLinearMap.inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
        Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL ϕ ∘SL Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {x y : S.Relation}, x = y ↔ x.fst = y.fst ∧ x.snd = y.snd ∧ x.r ≍ y.r
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeFun_mapEquiv : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (g : P ≃ₐ[R] P'),
  ⇑(FractionalIdeal.mapEquiv g) = FractionalIdeal.map ↑g
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.liftAlgHom_apply : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {S : Type u_5} [inst_3 : Semiring S] [inst_4 : Algebra R S]
  (f : MultilinearMap R A S) (one : f 1 = 1) (mul : ∀ (x y : (i : ι) → A i), f (x * y) = f x * f y)
  (a : PiTensorProduct R fun i => A i), (PiTensorProduct.liftAlgHom f one mul) a = (PiTensorProduct.lift f) a
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDocElabInfo : Lean.Elab.DocElabInfo → Lean.Elab.Info
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.sub_sub_sub_comm : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
  AddCommute b c → AddCommute (-b) d → AddCommute (-c) d → a - b - (c - d) = a - c - (b - d)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∪ t₂).get? k = t₁.get? k
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairMap_mem_pairs : ∀ (σ : Type u_1) [inst : DecidableEq σ] [inst_1 : Fintype σ] {k : ℕ},
  ∀ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k,
    MvPolynomial.NewtonIdentities.pairMap✝ σ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_comap : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A : IntermediateField F E) (f : L →ₐ[F] E) (B : IntermediateField F L),
  (IntermediateField.comap f A).relfinrank B = A.relfinrank (IntermediateField.map f B)
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.leftStructure : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → {T : (L.sum L').Theory} → (M : T.ModelType) → L.Structure ↑M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, k ∉ t₂ → Std.DTreeMap.Const.get? (t₁ ∪ t₂) k = Std.DTreeMap.Const.get? t₁ k
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonLeanDiagnosticTag : Lean.ToJson Lean.Lsp.LeanDiagnosticTag
-- Mathlib.Analysis.RCLike.Basic
/-- The imaginary part of a K Cauchy sequence, as a real Cauchy sequence.  -/
RCLike.cauSeqIm : {K : Type u_1} → [inst : RCLike K] → CauSeq K norm → CauSeq ℝ abs