mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Parser
/-- Dump `proof` into `path`, either in the binary or non-binary LRAT format, depending on `binaryProofs`.
 -/
Std.Tactic.BVDecide.LRAT.dumpLRATProof : System.FilePath → Array Std.Tactic.BVDecide.LRAT.IntAction → Bool → IO Unit
-- Lean.Elab.DefView
Lean.Elab.Command.mkDefViewOfOpaque : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Elab.DefView
-- Aesop.Search.SearchM
Aesop.SearchM.State.mk.sizeOf_spec : ∀ {Q : Type} [inst : Aesop.Queue Q] [inst_1 : SizeOf Q] (iteration : Aesop.Iteration) (queue : Q)
  (maxRuleApplicationDepthReached : Bool),
  sizeOf { iteration := iteration, queue := queue, maxRuleApplicationDepthReached := maxRuleApplicationDepthReached } =
    1 + sizeOf iteration + sizeOf queue + sizeOf maxRuleApplicationDepthReached
-- Init.Core
/-- Monadically iterates over the contents of a collection `xs`, with a local state `b` and the
possibility of early termination. At each iteration, the body of the loop is provided with a proof
that the current element is in the collection.

Because a `do` block supports local mutable bindings along with `return`, and `break`, the monadic
action passed to `ForIn'.forIn'` takes a starting state in addition to the current element of the
collection with its membership proof. The action returns an updated state together with an
indication of whether iteration should continue or terminate. If the action returns
`ForInStep.done`, then `ForIn'.forIn'` should stop iteration and return the updated state. If the
action returns `ForInStep.yield`, then `ForIn'.forIn'` should continue iterating if there are
further elements, passing the updated state to the action.

More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the
Lean reference manual](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=monad-iteration-syntax).
 -/
ForIn'.forIn' : {m : Type u₁ → Type u₂} →
  {ρ : Type u} →
    {α : outParam (Type v)} →
      {d : outParam (Membership α ρ)} →
        [self : ForIn' m ρ α d] → {β : Type u₁} → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits a multiplication.  -/
Subgroup.mul : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → Mul ↥H
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Rel.of_mul : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (x y : M i),
  Monoid.CoprodI.Rel M (FreeMonoid.of ⟨i, x⟩ * FreeMonoid.of ⟨i, y⟩) (FreeMonoid.of ⟨i, x * y⟩)
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_iff_vadd_eq_of_mem : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g +ᵥ a ∈ B → g +ᵥ B = B
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_ite : ∀ {α : Type u} {ps : Std.Do.PostShape} {Q : Std.Do.PostCond α ps} (c : Prop) [inst : Decidable c]
  (t e : Std.Do.PredTrans ps α), (if c then t else e).apply Q = if c then t.apply Q else e.apply Q
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.root'.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  P.root' i = P.toLinearMap (P.root i)
-- Mathlib.Tactic.Linter.Lint
/-- Linter that checks whether a structure should be in Prop.
 -/
Batteries.Tactic.Lint.structureInType : Batteries.Tactic.Lint.Linter
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.coe_center : ∀ (M : Type u_1) [inst : AddZeroClass M], ↑(AddSubmonoid.center M) = Set.addCenter M
-- Mathlib.Data.Fin.Embedding
/-- The inclusion map `Fin n → ℕ` is an embedding.  -/
Fin.valEmbedding : {n : ℕ} → Fin n ↪ ℕ
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_comp_lift_eq_id : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : PerfectRing M p]
  [inst_6 : IsPRadical i p] [inst_7 : ExpChar L p] [inst_8 : IsPRadical j p] [inst_9 : PerfectRing L p],
  (PerfectRing.lift j i p).comp (PerfectRing.lift i j p) = RingHom.id L
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S : CategoryTheory.ShortComplex C} {left : S.LeftHomologyData} {right : S.RightHomologyData} {iso : left.H ≅ right.H}
  {comm :
    autoParam
      (CategoryTheory.CategoryStruct.comp left.π (CategoryTheory.CategoryStruct.comp iso.hom right.ι) =
        CategoryTheory.CategoryStruct.comp left.i right.p)
      CategoryTheory.ShortComplex.HomologyData.comm._autoParam}
  {left_1 : S.LeftHomologyData} {right_1 : S.RightHomologyData} {iso_1 : left_1.H ≅ right_1.H}
  {comm_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp left_1.π (CategoryTheory.CategoryStruct.comp iso_1.hom right_1.ι) =
        CategoryTheory.CategoryStruct.comp left_1.i right_1.p)
      CategoryTheory.ShortComplex.HomologyData.comm._autoParam},
  { left := left, right := right, iso := iso, comm := comm } =
      { left := left_1, right := right_1, iso := iso_1, comm := comm_1 } →
    left = left_1 ∧ right = right_1 ∧ iso ≍ iso_1
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumComm_inr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_9)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (n : WithTop ℕ∞) (M' : Type u_13)
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'], ⇑(Diffeomorph.sumComm I M n M') ∘ Sum.inr = Sum.inl
-- Mathlib.CategoryTheory.Localization.Construction
/-- If `W : MorphismProperty C`, `LocQuiver W` is a quiver with the same objects
as `C`, and whose morphisms are those in `C` and placeholders for formal
inverses of the morphisms in `W`.  -/
CategoryTheory.Localization.Construction.LocQuiver : {C : Type uC} → [inst : CategoryTheory.Category.{uC', uC} C] → CategoryTheory.MorphismProperty C → Type uC
-- Init.Data.Vector.Lemmas
Vector.pop_append_of_size_ne_zero : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} (h : m ≠ 0),
  (xs ++ ys).pop = Vector.cast ⋯ (xs ++ ys.pop)
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the forward direction of `wbtw_comm`. -/
Wbtw.symm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {x y z : P}, Wbtw R x y z → Wbtw R z y x
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.image : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4}
  [inst_2 : SMul H Y] {φ : G → H} (j : X →ₑ[φ] Y),
  Function.Surjective φ → Function.Injective ⇑j → MulAction.IsBlock G B → MulAction.IsBlock H (⇑j '' B)
-- Mathlib.Condensed.Light.Functors
lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_apply_hom_hom : ∀ (X : LightProfinite) (X_1 : LightProfiniteᵒᵖ)
  (f : (topCatToLightCondSet.obj (LightProfinite.toTopCat.obj X)).obj.obj X_1),
  TopCat.Hom.hom
      ((CategoryTheory.ConcreteCategory.hom
            ((lightProfiniteToLightCondSetIsoTopCatToLightCondSet.inv.app X).hom.app X_1))
          f).hom =
    f
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
succ_mul_catalan_eq_centralBinom : ∀ (n : ℕ), (n + 1) * catalan n = n.centralBinom
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand the square  -/
norm_add_mul_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * RCLike.re (inner 𝕜 x y) + ‖y‖ * ‖y‖
-- Mathlib.Analysis.Normed.Group.Basic
mul_mem_ball_mul_iff : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ} {c : E},
  a * c ∈ Metric.ball (b * c) r ↔ a ∈ Metric.ball b r
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instVAddAssocClass : ∀ {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] [inst_7 : VAdd R' X] [inst_8 : VAdd R' M]
  [inst_9 : VAddAssocClass R' M M] [inst_10 : VAddAssocClass R' M X] [inst_11 : VAdd R R'] [VAddAssocClass R R' M],
  VAddAssocClass R R' (AddOreLocalization S X)
-- Mathlib.Order.Ideal
/-- The smallest ideal containing a given element.  -/
Order.Ideal.principal : {P : Type u_1} → [inst : Preorder P] → P → Order.Ideal P
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instLineDerivAdd : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F], LineDerivAdd E (TemperedDistribution E F) (TemperedDistribution E F)
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleDecl.mk.sizeOf_spec : ∀ (info : Lean.ConstantInfo) (kind : Lean.MetaM Lean.Lsp.CompletionItemKind)
  (tags : Lean.MetaM (Array Lean.Lsp.CompletionItemTag)),
  sizeOf { info := info, kind := kind, tags := tags } = 1 + sizeOf info
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The base ring is a right identity for the tensor product of algebra, up to algebra isomorphism.

Note that if `A` is commutative this can be instantiated with `S = A`.
 -/
Algebra.TensorProduct.rid : (R : Type uR) →
  (S : Type uS) →
    (A : Type uA) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                [inst_5 : Algebra S A] → [inst_6 : IsScalarTower R S A] → TensorProduct R A R ≃ₐ[S] A
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_add : ∀ {w i : ℕ} (x y : BitVec w), i ≤ w → BitVec.setWidth i (x + y) = BitVec.setWidth i x + BitVec.setWidth i y
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.IsEquiv.of_eq : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedAddCommMonoidWithTop Γ₀] [inst_1 : Ring R]
  {v v' : AddValuation R Γ₀}, v = v' → v.IsEquiv v'
-- Mathlib.RingTheory.Valuation.Basic
/-- If `v` is a valuation on a division ring then `v(x) = 0` iff `x = 0`.  -/
Valuation.zero_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀]
  (v : Valuation K Γ₀) {x : K}, v x = 0 ↔ x = 0
-- Mathlib.Control.Bifunctor
LawfulBifunctor.bimap_id_id : ∀ {F : Type u₀ → Type u₁ → Type u₂} {inst : Bifunctor F} [self : LawfulBifunctor F] {α : Type u₀} {β : Type u₁},
  bimap id id = id
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.verify₂_eq_isSome_assemble₂ : ∀ {w x : UInt8}, ByteArray.utf8DecodeChar?.verify₂ w x = (ByteArray.utf8DecodeChar?.assemble₂ w x).isSome
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the open ball of radius `r ≤ ∞` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.taylorSeries_eq_on_eball' : ∀ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ ⦃z : ℂ⦄,
  z ∈ Metric.eball c r →
    ∀ {f : ℂ → ℂ},
      DifferentiableOn ℂ f (Metric.eball c r) → ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  (a : (a : α) × β a) {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.minEntry? l = some a ↔
      a ∈ l ∧ ∀ (b : α), Std.Internal.List.containsKey b l = true → (compare a.fst b).isLE = true)
-- Mathlib.Probability.Kernel.Invariance
/-- A measure `μ` is invariant with respect to the kernel `κ` if the push-forward measure of `μ`
along `κ` equals `μ`.  -/
ProbabilityTheory.Kernel.Invariant : {α : Type u_1} → {mα : MeasurableSpace α} → ProbabilityTheory.Kernel α α → MeasureTheory.Measure α → Prop
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
/-- For a spectral object indexed by a preorder, this is the isomorphism
`E^{n₁}(i₀ ≤ i₂ ≤ i₃ ≤ i₄) ≅ E^{n₁}(i₁ ≤ i₂ ≤ i₃ ≤ i₄)`
when `H^{n₁ + 1}(i₀ ≤ i₁)` is a zero object.  -/
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀' : {C : Type u_1} →
  {ι' : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : Preorder ι'] →
          (X' : CategoryTheory.Abelian.SpectralObject C ι') →
            (i₀ i₁ i₂ i₃ i₄ : ι') →
              (hi₀₁ : i₀ ≤ i₁) →
                (hi₁₂ : i₁ ≤ i₂) →
                  (hi₂₃ : i₂ ≤ i₃) →
                    (hi₃₄ : i₃ ≤ i₄) →
                      (n₀ n₁ n₂ : ℤ) →
                        CategoryTheory.Limits.IsZero
                            ((X'.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁))) →
                          (hn₁ :
                              autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'._auto_1) →
                            (hn₂ :
                                autoParam (n₁ + 1 = n₂)
                                  CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'._auto_3) →
                              X'.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃)
                                  (CategoryTheory.homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ≅
                                X'.E (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃)
                                  (CategoryTheory.homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option (β a) → Option (β a)}, Std.DHashMap.Internal.Raw.WFImp ↑(m.alter a f)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_map : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (e : ι ↪ κ) (f : κ → M),
  ∏ x ∈ Finset.map e s, f x = ∏ x ∈ s, f (e x)
-- Mathlib.Analysis.Real.Pi.Bounds
/-- From a lower bound on `sqrtTwoAddSeries 0 n = 2 cos (π / 2 ^ (n+1))` of the form
`2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n`, one can deduce the upper bound
`π < a` thanks to basic trigonometric formulas as expressed in `pi_lt_sqrtTwoAddSeries`.  -/
Real.pi_upper_bound_start : ∀ (n : ℕ) {a : ℝ}, 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n → 1 / 4 ^ n ≤ a → Real.pi < a
-- Mathlib.Tactic.SimpIntro
/-- The `simp_intro` tactic is a combination of `simp` and `intro`: it will simplify the types of
variables as it introduces them and uses the new variables to simplify later arguments
and the goal.
* `simp_intro x y z` introduces variables named `x y z`
* `simp_intro x y z ..` introduces variables named `x y z` and then keeps introducing `_` binders
* `simp_intro (config := cfg) (discharger := tac) x y .. only [h₁, h₂]`:
  `simp_intro` takes the same options as `simp` (see `simp`)
  ```
  example : x + 0 = y → x = z := by
    simp_intro h
    -- h: x = y ⊢ y = z
    sorry
  ```
 -/
Mathlib.Tactic.«tacticSimp_intro_____..Only_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) (x : B'),
  ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).mapId x).inv.iso.inv = (F.mapId x).hom
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.le_of_opNorm_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  {f : ContinuousMultilinearMap 𝕜 E G} {C : ℝ}, ‖f‖ ≤ C → ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.smul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (r : ENNReal),
  ν.MutuallySingular μ → (r • ν).MutuallySingular μ
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.not_ge_of_lt : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b : α}, a < b → ¬b ≤ a
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
/-- The subtype of matrices with fixed determinant `m`  -/
FixedDetMatrix : (n : Type u_1) → [DecidableEq n] → [Fintype n] → (R : Type u_2) → [CommRing R] → R → Type (max 0 u_1 u_2)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
completeSpace_coe_iff_isComplete : ∀ {α : Type u} [inst : UniformSpace α] {s : Set α}, CompleteSpace ↑s ↔ IsComplete s
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_two_mul : ∀ (x : ℂ), Complex.sinh (2 * x) = 2 * Complex.sinh x * Complex.cosh x
-- Mathlib.RingTheory.PicardGroup
/-- The canonical isomorphism between a module and the result of tensoring it
from the right by two mutually dual invertible modules.  -/
Module.Invertible.rightCancelEquiv : {R : Type u} →
  {M : Type v} →
    {N : Type u_1} →
      (P : Type u_2) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      (TensorProduct R M N ≃ₗ[R] R) → TensorProduct R (TensorProduct R P M) N ≃ₗ[R] P
-- Std.Time.Zoned.TimeZone
/-- Converts a `WallTime` to a `Timestamp` given a timezone `offset`. The `WallTime` is treated as
civil time at the given offset: `UTC = wall − offset`.
 -/
Std.Time.WallTime.toTimestamp : Std.Time.WallTime → Std.Time.TimeZone.Offset → Std.Time.Timestamp
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- On a finite-dimensional space, an injective linear map is surjective.  -/
LinearMap.surjective_of_injective : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {f : V →ₗ[K] V}, Function.Injective ⇑f → Function.Surjective ⇑f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.isEmpty = false → ∀ {km : α}, t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Lean.Compiler.MetaAttr
/-- Returns true iff the user has declared the given declaration as `meta`.  -/
Lean.isMarkedMeta : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- The property of reflecting products expressed in terms of fans.  -/
CategoryTheory.Limits.isLimitOfIsLimitFanMkObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Discrete.functor f) G] →
                {P : C} →
                  (g : (j : J) → P ⟶ f j) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j)) →
                      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk P g)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.norm_unit_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (u : (NumberField.RingOfIntegers K)ˣ)
  (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.norm (u • x) = NumberField.mixedEmbedding.norm x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α] {k : α}
  (h : k ∈ m), m.getKey k h = k
-- Mathlib.Order.Preorder.Chain
/-- In this file, we use `≺` as a local notation for any relation `r`.  -/
_private.Mathlib.Order.Preorder.Chain.0.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.AdjoinRoot
/-- Adjoin a root of a polynomial `f` to a commutative ring `R`. We define the new ring
as the quotient of `R[X]` by the principal ideal generated by `f`.  -/
AdjoinRoot : {R : Type u_1} → [inst : CommRing R] → Polynomial R → Type u_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffOn.rpow_const_of_ne : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {p : ℝ}
  {n : WithTop ℕ∞}, ContDiffOn ℝ n f s → (∀ x ∈ s, f x ≠ 0) → ContDiffOn ℝ n (fun x => f x ^ p) s
-- Mathlib.Data.List.Range
/-- The members of `l.ranges` are pairwise disjoint  -/
List.ranges_disjoint : ∀ (l : List ℕ), List.Pairwise List.Disjoint l.ranges
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli.eq_1 : ∀ (n : ℕ),
  Polynomial.bernoulli n = ∑ i ∈ Finset.range (n + 1), (Polynomial.monomial (n - i)) (bernoulli i * ↑(n.choose i))
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
uliftZPowersHom_apply_apply : ∀ (G : Type u) [inst : Group G] (a : G) (x : ULift.{u, 0} (Multiplicative ℤ)),
  ((uliftZPowersHom G) a) x = a ^ Multiplicative.toAdd (MulEquiv.ulift x)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_restrict_mono_set : ∀ {E : Type u_3} [inst : SeminormedAddCommGroup E] {X : Type u_4} [inst_1 : TopologicalSpace X] (f : C(X, E))
  {K L : TopologicalSpace.Compacts X}, K ≤ L → ‖ContinuousMap.restrict (↑K) f‖ ≤ ‖ContinuousMap.restrict (↑L) f‖
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompιWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)],
  (HomotopicalAlgebra.CofibrantObject.ι.comp L).IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject C))
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.hom_ext : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  (g₁ g₂ : S →+* WittVector p R),
  (∀ (k : ℕ), (WittVector.truncate k).comp g₁ = (WittVector.truncate k).comp g₂) → g₁ = g₂
-- Mathlib.Topology.ClusterPt
ClusterPt.frequently' : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop},
  ClusterPt x F → (∀ᶠ (y : X) in F, p y) → ∃ᶠ (y : X) in nhds x, p y
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RcoSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] [inst_1 : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (range : Std.Rco α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).vec.get idx ⋯ =
    (s.get idx hidx).cast ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_int_mul_pi : ∀ (n : ℤ), Real.tan (↑n * Real.pi) = 0