mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- An inductive principle for the elements of `generateMeasurableRec`.  -/
MeasurableSpace.generateMeasurableRec_induction : ∀ {α : Type u} {s : Set (Set α)} {i : Ordinal.{u_1}} {t : Set α} {p : Set α → Prop},
  (∀ t ∈ s, p t) →
    p ∅ →
      (∀ (u : Set α), p u → (∃ j < i, u ∈ MeasurableSpace.generateMeasurableRec s j) → p uᶜ) →
        (∀ (f : ℕ → Set α),
            (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ MeasurableSpace.generateMeasurableRec s j) → p (⋃ n, f n)) →
          t ∈ MeasurableSpace.generateMeasurableRec s i → p t
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- The component 1-morphisms of a strong transformation.  -/
CategoryTheory.Pseudofunctor.StrongTrans.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} → F.StrongTrans G → (a : B) → F.obj a ⟶ G.obj a
-- Mathlib.Topology.MetricSpace.Dilation
/-- Copy of a `Dilation` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
Dilation.copy : {α : Type u_1} →
  {β : Type u_2} →
    [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → (f : α →ᵈ β) → (f' : α → β) → f' = ⇑f → α →ᵈ β
-- Mathlib.Algebra.Group.Units.Defs
divp_inv : ∀ {α : Type u} [inst : Monoid α] {a : α} (u : αˣ), a /ₚ u⁻¹ = a * ↑u
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.copy : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → p.copy.Splits t₁ t₂
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.instDistribMulActionSubtypeMemTorsion' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (S : Type u_3) →
            [inst_3 : CommMonoid S] →
              [inst_4 : DistribMulAction S M] →
                [inst_5 : SMulCommClass S R M] → DistribMulAction S ↥(Submodule.torsion' R M S)
-- Lean.Meta.Tactic.Grind.Types
/-- Solver states.  -/
Lean.Meta.Grind.GoalState.sstates : Lean.Meta.Grind.GoalState → Array Lean.Meta.Grind.SolverExtensionState
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).hom = Y.left.hom
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_le_pi_mul_log : ∀ (n : ℕ), Chebyshev.theta ↑n ≤ ↑n.primeCounting * Real.log ↑n
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.prodEquiv_symm_apply : ∀ {α : Type u_1} (s : Finset α), Set.powersetCard.prodEquiv.symm s = ⟨s.card, Set.powersetCard.ofCard ⋯⟩
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.K'.elim.match_1.eq_2 : ∀ (motive : Turing.PartrecToTM2.K' → Sort u_1) (h_1 : Unit → motive Turing.PartrecToTM2.K'.main)
  (h_2 : Unit → motive Turing.PartrecToTM2.K'.rev) (h_3 : Unit → motive Turing.PartrecToTM2.K'.aux)
  (h_4 : Unit → motive Turing.PartrecToTM2.K'.stack),
  (match Turing.PartrecToTM2.K'.rev with
    | Turing.PartrecToTM2.K'.main => h_1 ()
    | Turing.PartrecToTM2.K'.rev => h_2 ()
    | Turing.PartrecToTM2.K'.aux => h_3 ()
    | Turing.PartrecToTM2.K'.stack => h_4 ()) =
    h_2 ()
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.diagram_obj : ∀ (P : ProfiniteAddGrp.{u}) (X : OpenNormalAddSubgroup ↑P.toProfinite.toTop),
  P.diagram.obj X = (CategoryTheory.forget₂ FiniteAddGrp.{u} ProfiniteAddGrp.{u}).obj (P.toFiniteQuotientFunctor.obj X)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.diagonal_fin_one : ∀ {α : Type u} [inst : Zero α] (d : Fin 1 → α), Matrix.diagonal d = !![d 0]
-- Mathlib.Algebra.Order.Ring.Canonical
CanonicallyOrderedAdd.toMulRightMono : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [inst_1 : LE R] [CanonicallyOrderedAdd R], MulRightMono R
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_pair : ∀ {M : Type u_3} [inst : CommMonoid M] (a b : M), {a, b}.prod = a * b
-- Init.Data.Nat.Simproc
Nat.Simproc.eq_add_le : ∀ {a : ℕ} (b : ℕ) {c : ℕ}, c ≤ a → (a = b + c) = (b = a - c)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_rio' : ∀ {n k : ℕ}, Array.map (fun x => k + x) (*...n).toArray = (k...k + n).toArray
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_mul' : ∀ {R : Type u} {σ : Type u_1} {a : R} [inst : CommSemiring R] {p : MvPolynomial σ R}, MvPolynomial.C a * p = a • p
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.toEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_2 : ∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
  [inst_3 : ∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)], adj.toEquivalence.functor = F
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse.  -/
Orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle (x + y) y).sin = ‖x + y‖
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- The inclusion of a quiver `V` into its path category, as a prefunctor.
 -/
CategoryTheory.Paths.of : (V : Type u₁) → [inst : Quiver V] → V ⥤q CategoryTheory.Paths V
-- Init.Data.String.Modify
/-- The position just after the position that changed in a `Pos.set` call.  -/
String.Pos.pastSet : {s : String} → (p : s.Pos) → (c : Char) → (hp : p ≠ s.endPos) → (p.set c hp).Pos
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.ofArrowIso_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Y₁ Y₂ : C} {f' : Y₁ ⟶ Y₂}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') (a : c.ι), (c.ofArrowIso e).π a = c.π a
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
PiLp.hasFDerivAt_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [Finite ι] (p : ENNReal)
  [Fact (1 ≤ p)] (f : PiLp p E) (i : ι), HasFDerivAt (fun f => f.ofLp i) (PiLp.proj p E i) f
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasure.average : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.IsFiniteMeasure ((μ Set.univ)⁻¹ • μ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getKey! k = default
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.instInhabited : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : Star A] → Inhabited (A →⋆ₐ[R] A)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.main : Lean.MVarId → Lean.Meta.Grind.Params → Lean.MetaM Lean.Meta.Grind.Result
-- Lean.Expr
Lean.instEmptyCollectionMVarIdMap : {α : Type} → EmptyCollection (Lean.MVarIdMap α)
-- Mathlib.RingTheory.HahnSeries.Basic
/-- Change a `HahnSeries` with coefficients in a `HahnSeries` to a `HahnSeries` on a Lex product.  -/
HahnSeries.ofIterate : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      [inst : PartialOrder Γ] →
        [inst_1 : Zero R] → [inst_2 : PartialOrder Γ'] → HahnSeries Γ (HahnSeries Γ' R) → HahnSeries (Lex (Γ × Γ')) R
-- Init.Data.Int.Pow
Int.sq_nonneg : ∀ (m : ℤ), 0 ≤ m ^ 2
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The tensor product `A ⊗[ℤ] B` forms a cocone for `A` and `B`.  -/
CommRingCat.coproductCocone : (A B : CommRingCat) → CategoryTheory.Limits.BinaryCofan A B
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntry.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
      false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l l_2 : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_3 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l_2 = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r))
                          h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r), h with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l l_2@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r), h_3 =>
      h_2 size k v l l_2 size_2 k_2 v_2 l_3 r h h_3) =
    h_2 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ h
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) CategoryTheory.Limits.prod.fst =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f
-- Mathlib.Algebra.Quaternion
Quaternion.star_add_self : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), star a + a = 2 * ↑a.re
-- Mathlib.Logic.Function.Basic
/-- A relation `r : α → β → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some function `f`.  -/
forall_existsUnique_iff : ∀ {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop}, (∀ (a : α), ∃! b, r a b) ↔ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules)
  (U : (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Opens) {Z : ModuleCat ↑R}
  (h : (AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.obj (Opposite.op U) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.tilde.toOpen ((AlgebraicGeometry.modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)) U)
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.modulesSpecToSheaf.map M.fromTildeΓ).hom.app (Opposite.op U)) h) =
    CategoryTheory.CategoryStruct.comp
      ((AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.map (CategoryTheory.homOfLE ⋯).op) h
-- Mathlib.RingTheory.Invariant.Galois
/-- In the AKLB setup, the Galois group of `L/K` acts on `B`.  -/
IsIntegralClosure.MulSemiringAction : (A : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      (B : Type u_4) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : Field K] →
              [inst_3 : Field L] →
                [inst_4 : Algebra A K] →
                  [inst_5 : Algebra B L] →
                    [IsFractionRing A K] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : Algebra K L] →
                          [inst_9 : Algebra A L] →
                            [IsScalarTower A K L] →
                              [IsScalarTower A B L] →
                                [IsIntegralClosure B A L] → [Algebra.IsAlgebraic K L] → MulSemiringAction Gal(L/K) B
-- Mathlib.Combinatorics.SimpleGraph.Circulant
SimpleGraph.circulantGraph_eq_erase_zero : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), SimpleGraph.circulantGraph s = SimpleGraph.circulantGraph (s \ {0})
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits an inverse.  -/
InvMemClass.inv : {G : Type u_5} → {S : Type u_6} → [inst : Inv G] → [inst_1 : SetLike S G] → [InvMemClass S G] → {H : S} → Inv ↥H
-- Mathlib.NumberTheory.NumberField.Basic
/-- Given `f : M →* K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function
`M →* 𝓞 K`.  -/
NumberField.RingOfIntegers.restrict_monoidHom : {K : Type u_1} →
  [inst : Field K] →
    {M : Type u_3} →
      [inst_1 : MulOneClass M] → (f : M →* K) → (∀ (x : M), IsIntegral ℤ (f x)) → M →* NumberField.RingOfIntegers K
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitMulOneClass : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) → [CategoryTheory.IsFiltered J] → MulOneClass (MonCat.FilteredColimits.M F)
-- Mathlib.SetTheory.Cardinal.ENat
/-- **Alias** of the reverse direction of `Cardinal.ofENat_le_ofENat`. -/
Cardinal.ofENat_le_ofENat_of_le : ∀ {m n : ℕ∞}, m ≤ n → ↑m ≤ ↑n
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- the condition that `s` is a section of `S.g`  -/
CategoryTheory.ShortComplex.Splitting.s_g_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (self : S.Splitting) {Z : C} (h : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.s (CategoryTheory.CategoryStruct.comp S.g h) = h
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ext_getKey_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m₁ m₂ : Std.ExtHashMap α β},
  (∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') → (∀ (k : α), m₁[k]? = m₂[k]?) → m₁ = m₂
-- Lean.Meta.Tactic.Injection
Lean.Meta.injectionIntro : Lean.MVarId → ℕ → List Lean.Name → optParam Bool true → Lean.MetaM Lean.Meta.InjectionResult
-- Mathlib.Data.Setoid.Basic
/-- The kernel of a function is an equivalence relation.  -/
Setoid.ker : {α : Type u_1} → {β : Type u_2} → (α → β) → Setoid α
-- Mathlib.Probability.CDF
/-- The cdf is monotone.  -/
ProbabilityTheory.monotone_cdf : ∀ (μ : MeasureTheory.Measure ℝ), Monotone ↑(ProbabilityTheory.cdf μ)
-- Mathlib.Analysis.Distribution.Distribution
/-- We denote `𝓓'(Ω, F)` the space of `F`-valued distributions on `Ω`. Note that using `𝓓'`
is a bit abusive since this is no longer a dual space unless `F = 𝕜`.  -/
Distributions.«term𝓓'(_,_)» : Lean.ParserDescr
-- Mathlib.Dynamics.Ergodic.Extreme
Ergodic.iff_mem_extremePoints : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X}
  [MeasureTheory.IsProbabilityMeasure μ],
  Ergodic f μ ↔
    μ ∈ Set.extremePoints ENNReal {ν | MeasureTheory.MeasurePreserving f ν ν ∧ MeasureTheory.IsProbabilityMeasure ν}
-- Init.System.IO
/-- Files that are neither ordinary files, directories, or symbolic links.  -/
IO.FS.FileType.other : IO.FS.FileType
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.IsSeparated f],
  AlgebraicGeometry.IsSeparated (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Init.Prelude
/-- Converts a `TSyntaxArray` to an `Array Syntax`, without reallocation.  -/
Lean.TSyntaxArray.raw : {ks : Lean.SyntaxNodeKinds} → Lean.TSyntaxArray ks → Array Lean.Syntax
-- Mathlib.Algebra.Opposites
MulOpposite.op_inv : ∀ {α : Type u_1} [inst : Inv α] (x : α), MulOpposite.op x⁻¹ = (MulOpposite.op x)⁻¹
-- Lean.Parser.Term
Lean.Parser.Termination.coinductiveFixpoint.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- An isomorphism between isocrystals respects the Frobenius map.

Notation `M ≃ᶠⁱ [p, k]` in the `Isocrystal` namespace.  -/
Isocrystal.«term_≃ᶠⁱ[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (e : T ≅ T')
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₂ = e.inv.hom₂
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.inter m₂).getKey! k = default
-- Lean.DocString.DeferredCheck
/-- The reference's source text, to quote in error messages.  -/
Lean.Doc.DeferredCheck.sourceString : Lean.Doc.DeferredCheck → String
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- An element is in the closure of a two-element set if it is a linear combination of
those two elements.  -/
AddSubmonoid.mem_closure_pair : ∀ {A : Type u_4} [inst : AddCommMonoid A] (a b c : A), c ∈ AddSubmonoid.closure {a, b} ↔ ∃ m n, m • a + n • b = c
-- Mathlib.Data.Set.Prod
Set.range_prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ},
  Set.range (Prod.map m₁ m₂) = Set.range m₁ ×ˢ Set.range m₂
-- Mathlib.GroupTheory.Perm.Fin
Fin.isThreeCycle_cycleRange_two : ∀ {n : ℕ}, (Fin.cycleRange 2).IsThreeCycle
-- Mathlib.Algebra.Module.Torsion.Basic
/-- Any module is also a module over the quotient of the ring by the annihilator.
Not an instance because it causes synthesis failures / timeouts.  -/
Module.quotientAnnihilator : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module (R ⧸ Module.annihilator R M) M
-- Mathlib.Analysis.Complex.Isometry
rotationOf_rotation : ∀ (a : Circle), rotationOf (rotation a) = a
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.ideal_gc : ∀ (X : Type u_1) (R : Type u_2) [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R], GaloisConnection ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet R)
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
  (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0),
  R.extEquivCohomologyClass (R.extMk f m hm hf) =
    CochainComplex.HomComplex.CohomologyClass.mk
      (CochainComplex.HomComplex.Cocycle.fromSingleMk
        (CategoryTheory.CategoryStruct.comp f (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)
-- Lean.Parser.Term
Lean.Parser.Term.borrowed.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Sym.Sym2
Sym2.mem_fromRel_irrefl_other_ne : ∀ {α : Type u_1} {r : α → α → Prop} {sym : Std.Symm r},
  Std.Irrefl r → ∀ {a : α} {z : Sym2 α}, z ∈ Sym2.fromRel sym → ∀ (h : a ∈ z), Sym2.Mem.other h ≠ a
-- Init.Data.Order.Lemmas
Std.le_of_not_ge : ∀ {α : Type u} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2] {a b : α}, ¬b ≤ a → a ≤ b
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.wellPowered_of_equiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) [inst_2 : CategoryTheory.LocallySmall.{w, v, u₁} C] [inst_3 : CategoryTheory.LocallySmall.{w, v₂, u₂} D]
  [CategoryTheory.WellPowered.{w, v, u₁} C], CategoryTheory.WellPowered.{w, v₂, u₂} D
-- Mathlib.Data.Finsupp.Basic
/-- Given `l`, a finitely supported function from the sigma type `Σ (i : ι), αs i` to `β`,
`split_support l` is the finset of indices in `ι` that appear in the support of `l`.  -/
Finsupp.splitSupport : {ι : Type u_4} → {M : Type u_5} → {αs : ι → Type u_12} → [inst : Zero M] → ((i : ι) × αs i →₀ M) → Finset ι
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.isPiSystem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)],
  IsPiSystem (MeasureTheory.measurableCylinders α)
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_hom_fst : ∀ (X Y : TopCat),
  CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).hom TopCat.prodFst = CategoryTheory.Limits.prod.fst
-- Mathlib.RingTheory.LinearDisjoint
/-- In a commutative ring, if subalgebras `A` and `B` are linearly disjoint and they are
free modules, then the rank of `A ⊔ B` is equal to the product of the rank of `A` and `B`.  -/
Subalgebra.LinearDisjoint.rank_sup_of_free : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Free R ↥A] [Module.Free R ↥B], Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B
-- Mathlib.NumberTheory.Niven
/-- Niven's theorem, but stated for `sin` instead of `cos`.  -/
niven_sin : ∀ {θ : ℝ}, (∃ r, θ = ↑r * Real.pi) → (∃ q, Real.sin θ = ↑q) → Real.sin θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}
-- Init.Data.Nat.Basic
Nat.le_or_eq_of_le_succ : ∀ {m n : ℕ}, m ≤ n.succ → m ≤ n ∨ m = n.succ
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.instSupSetColexForall : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] → [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedGT ι] → SupSet (Colex ((i : ι) → α i))
-- Mathlib.LinearAlgebra.Dual.Defs
Module.dualMap_dualMap_eq_iff_of_injective : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsReflexive R M] {M' : Type u_6} [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] {f g : M →ₗ[R] M'},
  Function.Injective ⇑(Module.Dual.eval R M') → (f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddLocalization.addEquivOfQuotient_symm_addMonoidOf : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (x : M),
  (AddLocalization.addEquivOfQuotient f).symm (f x) = (AddLocalization.addMonoidOf S) x
-- Lean.Declaration
Lean.OpaqueVal.value : Lean.OpaqueVal → Lean.Expr