mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Stats.Extension
/-- The Aesop call for which stats were collected.
 -/
Aesop.StatsExtensionEntry.aesopStx : Aesop.StatsExtensionEntry → Lean.Syntax
-- Batteries.Data.AssocList
Batteries.AssocList.all.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool), Batteries.AssocList.all p Batteries.AssocList.nil = true
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_biInf : ∀ {α : Type u_1} (u : α → ℕ → ENNReal) {s : Set α},
  s.Finite → ExpGrowth.expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, ExpGrowth.expGrowthInf (u x)
-- Lean.Meta.Tactic.Grind.Theorems
/-- Marks the theorem with the given origin as `erased`  -/
Lean.Meta.Grind.Theorems.erase : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.Meta.Grind.Origin → Lean.Meta.Grind.Theorems α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- Forgets the first fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction₃.forgetFst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₃ X Y → W.LeftFraction₂ X Y
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.instFintypeSubtypeMemOfDecidablePred.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) [inst_1 : DecidablePred fun x => x ∈ K] [inst_2 : Fintype G],
  K.instFintypeSubtypeMemOfDecidablePred = inferInstance
-- Mathlib.Tactic.NormNum.NatFactorial
Mathlib.Meta.NormNum.isNat_factorial : ∀ {n x : ℕ},
  Mathlib.Meta.NormNum.IsNat n x → ∀ (a : ℕ), Nat.ascFactorial 1 x = a → Mathlib.Meta.NormNum.IsNat n.factorial a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constModify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ (k : α) (f : β → β), (Std.DTreeMap.Raw.Const.modify t₁ k f).Equiv (Std.DTreeMap.Raw.Const.modify t₂ k f)
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of December.
 -/
Std.Time.Month.Ordinal.december : Std.Time.Month.Ordinal
-- Init.Data.SInt.Bitwise
instCommutativeInt16HXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj)
  (hom :
    (i₁ i₂ : ι) → obj i₁ ⟶ (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (obj i₂)))
  (counit :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (hom i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (obj i)) =
          CategoryTheory.CategoryStruct.id (obj i))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit._autoParam)
  (coassoc :
    autoParam
      (∀ (i₁ i₂ i₃ : ι),
        CategoryTheory.CategoryStruct.comp (hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂ i₃))) =
          CategoryTheory.CategoryStruct.comp (hom i₁ i₃)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map
              ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (obj i₃)))))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc._autoParam)
  (obj_1 : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj)
  (hom_1 :
    (i₁ i₂ : ι) →
      obj_1 i₁ ⟶ (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (obj_1 i₂)))
  (counit_1 :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (hom_1 i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (obj_1 i)) =
          CategoryTheory.CategoryStruct.id (obj_1 i))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit._autoParam)
  (coassoc_1 :
    autoParam
      (∀ (i₁ i₂ i₃ : ι),
        CategoryTheory.CategoryStruct.comp (hom_1 i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom_1 i₂ i₃))) =
          CategoryTheory.CategoryStruct.comp (hom_1 i₁ i₃)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map
              ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (obj_1 i₃)))))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc._autoParam),
  ({ obj := obj, hom := hom, counit := counit, coassoc := coassoc } =
      { obj := obj_1, hom := hom_1, counit := counit_1, coassoc := coassoc_1 }) =
    (obj = obj_1 ∧ hom ≍ hom_1)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.integral_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧}
  {P : MeasureTheory.Measure Ω} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {X : Ω → 𝓧},
  ProbabilityTheory.HasLaw X μ P →
    ∀ {f : 𝓧 → E}, MeasureTheory.AEStronglyMeasurable f μ → ∫ (x : Ω), (f ∘ X) x ∂P = ∫ (x : 𝓧), f x ∂μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_pi_div_two_sub : ∀ (θ : Real.Angle), (↑(Real.pi / 2) - θ).cos = θ.sin
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Relations.isUniversal_irreflexive : ∀ {L : FirstOrder.Language} (r : L.Relations 2), FirstOrder.Language.BoundedFormula.IsUniversal r.irreflexive
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.NoRepetition.append_singleton_of_ne : ∀ {α : Type u} {a b : α} {l : List α}, NoRepetition✝ a l → a ≠ b → NoRepetition✝ a (l ++ [b])
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertMany_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          ∀ {h' : Std.DTreeMap.Internal.Impl.contains k' ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) = true},
            Std.DTreeMap.Internal.Impl.Const.get (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k' h' = v
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.atIdxSlow?_eq_match.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Data.Sym.Sym2
Sym2.Rel.trans : ∀ {α : Type u_1} {x y z : α × α}, Sym2.Rel α x y → Sym2.Rel α y z → Sym2.Rel α x z
-- Init.Data.Order.Lemmas
Std.left_le_max : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α] [Std.Refl fun x1 x2 => x1 ≤ x2] [Std.LawfulOrderSup α] {a b : α},
  a ≤ a ⊔ b
-- Mathlib.Topology.Inseparable
SeparationQuotient.instOne.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : One X],
  SeparationQuotient.instOne = { one := SeparationQuotient.mk 1 }
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.red_iff_addIrreducible : ∀ {α : Type u} {L : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool},
  (x1, b1) ≠ (x2, b2) → (FreeAddGroup.Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)])
-- Init.Data.Fin.Lemmas
/-- This is not a global instance, but may be activated locally via `open Fin.NatCast in ...`.

This is not an instance because the `binop%` elaborator assumes that
there are no non-trivial coercion loops,
but this introduces a coercion from `Nat` to `Fin n` and back.

Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.
For example, for `x : Fin k` and `n : Nat`,
it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
silently introducing wraparound arithmetic.
 -/
Fin.NatCast.instNatCast : (n : ℕ) → [NeZero n] → NatCast (Fin n)
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.le_egirth : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ∞}, n ≤ G.egirth ↔ ∀ (a : α) (w : G.Walk a a), w.IsCycle → n ≤ ↑w.length
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive monoid homomorphism `f : M →+ N` such that `f x` additively commutes
with `f y` for all `x`, `y` defines an additive monoid homomorphism from `Mᵃᵒᵖ`.  -/
AddMonoidHom.fromOpposite : {M : Type u_3} →
  {N : Type u_4} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → (f : M →+ N) → (∀ (x y : M), AddCommute (f x) (f y)) → Mᵃᵒᵖ →+ N
-- Mathlib.Algebra.Homology.Opposite
/-- The natural isomorphism `K.op.cycles i ≅ op (K.opcycles i)`.  -/
HomologicalComplex.cyclesOpNatIso : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          [inst_2 : CategoryTheory.CategoryWithHomology V] →
            (i : ι) →
              (HomologicalComplex.opFunctor V c).comp (HomologicalComplex.cyclesFunctor Vᵒᵖ c.symm i) ≅
                (HomologicalComplex.opcyclesFunctor V c i).op
-- Mathlib.Topology.Algebra.MulAction
/-- Eta-expanded form of `ContinuousWithinAt.smul` -/
ContinuousWithinAt.fun_smul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {b : Y} {s : Set Y},
  ContinuousWithinAt f s b → ContinuousWithinAt g s b → ContinuousWithinAt (fun i => f i • g i) s b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} →
            {h₂ : S₂.HomologyData} →
              CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left →
                CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right →
                  CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂
-- Mathlib.Order.Hom.Basic
OrderIso.coe_symm_toRelIsoGT : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), ⇑e.toRelIsoGT.symm = ⇑e.symm
-- Mathlib.Order.RelIso.Basic
RelEmbedding.prodLexMap_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  {u : δ → δ → Prop} (f : r ↪r s) (g : t ↪r u) (a : α × γ), (f.prodLexMap g) a = Prod.map (⇑f) (⇑g) a
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.comp_P_eq_self_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  CategoryTheory.CategoryStruct.comp φ ((AlgebraicTopology.DoldKan.P q).f (n + 1)) = φ ↔
    AlgebraicTopology.DoldKan.HigherFacesVanish q φ
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.eval_natCast_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R) (n : ℕ),
  Polynomial.eval (↑n) (Polynomial.map f p) = f (Polynomial.eval (↑n) p)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBase.isBase_insert_sdiff_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {B : Set α},
  M.IsBase B → e ∈ M.closure (insert f B \ {e}) → e ∈ insert f B → M.IsBase (insert f B \ {e})
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integral_fun_fst : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] (f : α → E),
  ∫ (z : α × β), f z.1 ∂μ.prod ν = ν.real Set.univ • ∫ (x : α), f x ∂μ
-- Mathlib.Combinatorics.Graph.Basic
/-- Two graphs are compatible if their shared edges have the same ends in both graphs.  -/
Graph.Compatible : {α : Type u_1} → {β : Type u_2} → Graph α β → Graph α β → Prop
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.lifts_iff_ringHom_rangeS : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} (p : Polynomial S),
  p ∈ Polynomial.lifts f ↔ p ∈ (Polynomial.mapRingHom f).rangeS
-- Mathlib.Data.Int.SuccPred
Int.instPredOrder : PredOrder ℤ
-- Mathlib.Data.Set.FiniteExhaustion
/-- The union of all sets in a `FiniteExhaustion` equals `s`  -/
Set.FiniteExhaustion.iUnion_eq' : ∀ {α : Type u_1} {s : Set α} (self : s.FiniteExhaustion), ⋃ n, self.toFun n = s
-- Init.Data.List.Zip
List.unzip_replicate : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {a : α} {b : β},
  (List.replicate n (a, b)).unzip = (List.replicate n a, List.replicate n b)
-- Std.Data.Iterators.Producers.Monadic.Array
/-- Internal implementation detail of the iterator library.  -/
Std.Iterators.Types.ArrayIterator.array : {α : Type w} → Std.Iterators.Types.ArrayIterator α → Array α
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sq_eq_sq_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a b : A),
  autoParam (0 ≤ a) CFC.sq_eq_sq_iff._auto_1 → autoParam (0 ≤ b) CFC.sq_eq_sq_iff._auto_3 → (a ^ 2 = b ^ 2 ↔ a = b)
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.Nat.xgcdAux.match_1.eq_1 : ∀ (motive : (n : ℕ) → ((m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → Sort u_1)
  (ih : (m : ℕ) → m < 0 → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
  (h_1 : (ih : (m : ℕ) → m < 0 → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive 0 ih)
  (h_2 : (k : ℕ) → (ih : (m : ℕ) → m < k.succ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive k.succ ih),
  (match 0, ih with
    | 0, ih => h_1 ih
    | k.succ, ih => h_2 k ih) =
    h_1 ih
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.matrixEquiv_apply : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : ⨁ f ⟶ ⨁ g) (j : J) (k : K),
  CategoryTheory.Limits.biproduct.matrixEquiv m j k = CategoryTheory.Limits.biproduct.components m j k
-- Std.Time.Format.Modifier
Std.Time.instReprZoneId : Repr Std.Time.ZoneId
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey! k = default
-- Mathlib.Computability.Reduce
ManyOneDegree.add_of : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {β : Type v} [inst_2 : Primcodable β]
  [inst_3 : Inhabited β] (p : Set α) (q : Set β),
  ManyOneDegree.of (Sum.elim p q) = ManyOneDegree.of p + ManyOneDegree.of q
-- Mathlib.RingTheory.Localization.Integral
/-- If the field `L` is an algebraic extension of the integral domain `A`,
the integral closure `C` of `A` in `L` has fraction field `L`.  -/
IsIntegralClosure.isFractionRing_of_algebraic : ∀ (A : Type u_3) [inst : CommRing A] {L : Type u_5} [inst_1 : Field L] [inst_2 : Algebra A L] (C : Type u_6)
  [inst_3 : CommRing C] [IsDomain C] [inst_5 : Algebra C L] [IsIntegralClosure C A L] [inst_7 : Algebra A C]
  [IsScalarTower A C L] [Algebra.IsAlgebraic A L], (∀ (x : A), (algebraMap A L) x = 0 → x = 0) → IsFractionRing C L
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {a : α}, ∅.getKey? a = none
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_of_mem_nhds_one_of_inv_mul_left_subset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {s s' t : Set G},
  s ∈ nhds 1 → (∀ x ∈ s, x⁻¹ ∈ s) → s * s' ⊆ t → closure s' ⊆ t
-- Init.Prelude
/-- Executes an `EStateM` action with the initial state `s`. The returned value includes the final state
and indicates whether an exception was thrown or a value was returned.
 -/
EStateM.run : {ε σ α : Type u} → EStateM ε σ α → σ → EStateM.Result ε σ α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.atIdx!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {i : ℕ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.atIdx! i = t₂.atIdx! i
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.modifyStruct : (Lean.Meta.Grind.Arith.Linear.Struct → Lean.Meta.Grind.Arith.Linear.Struct) → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Mathlib.Analysis.Complex.Basic
_private.Mathlib.Analysis.Complex.Basic.0.RCLike.termIC : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mk_radius : ∀ {P : Type u_2} [inst : MetricSpace P] (c : P) (r : ℝ), { center := c, radius := r }.radius = r
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- For any `k : K`, `y : L`, we have
`B.norm ((algebra_map K L) k * y) = B.norm ((algebra_map K L) k) * B.norm y`.  -/
Module.Basis.norm_smul : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_4}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {B : Module.Basis ι K L} {i : ι},
  B i = 1 → ∀ (k : K) (y : L), B.norm ((algebraMap K L) k * y) = B.norm ((algebraMap K L) k) * B.norm y
-- Batteries.Lean.Meta.InstantiateMVars
/-- Instantiate metavariables in the `LocalDecl` of the given fvar, update the
`LocalDecl` and return the new `LocalDecl.`
 -/
Lean.MVarId.instantiateMVarsInLocalDecl : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → [Lean.MonadError m] → Lean.MVarId → Lean.FVarId → m Lean.LocalDecl
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Given an invariant measure then it gives the same mass to measurable sets with
compact closure as any other invariant measure, up to the scalar `haarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which removes the
measurability assumption.  -/
MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  {s : Set G}, MeasurableSet s → IsCompact (closure s) → μ' s = μ'.haarScalarFactor μ • μ s
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.rightShift_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cocycle K L n) (a n' : ℤ) (hn' : n' + a = n),
  ↑(γ.rightShift a n' hn') = (↑γ).rightShift a n' hn'
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.interpretParserDescr' : Lean.ParserDescr → Lean.CoreM Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.PowerBasis
PowerBasis.coe_basis : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (pb : PowerBasis R S),
  ⇑pb.basis = fun i => pb.gen ^ ↑i
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_monic_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → (p * q).leadingCoeff = q.leadingCoeff
-- Init.Data.Range.Polymorphic.PRange
Std.Roo.mk.injEq : ∀ {α : Type u} (lower upper lower_1 upper_1 : α),
  ((lower<...upper) = lower_1<...upper_1) = (lower = lower_1 ∧ upper = upper_1)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective.  -/
AddSubmonoid.gciMapComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_4} →
          [inst_2 : FunLike F M N] →
            [mc : AddMonoidHomClass F M N] →
              {f : F} → Function.Injective ⇑f → GaloisCoinsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `max₃ j₁ j₂ j₃` is an arbitrary choice of object to the right of `j₁`, `j₂` and `j₃`,
whose existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.max₃ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.IsFilteredOrEmpty C] → C → C → C → C
-- Mathlib.Data.Finset.Lattice.Fold
Finset.exists_mem_eq_inf' : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} (H : s.Nonempty) (f : ι → α),
  ∃ i ∈ s, s.inf' H f = f i
-- Mathlib.Data.Nat.Find
Nat.lt_find_iff : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (n : ℕ), n < Nat.find h ↔ ∀ m ≤ n, ¬p m
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- **Alias** of `SSet.Homotopy.chainComplexMap`.

---

If `f` and `g` are homotopic maps of simplicial sets, then they induce chain-homotopic
maps on the singular chain complexes with coefficients in `R`.
 -/
SSet.Homotopy.singularChainComplexFunctorObjMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasCoproducts C] →
        {X Y : SSet} →
          {f g : X ⟶ Y} → SSet.Homotopy f g → (R : C) → Homotopy (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.IsIPCOfShape.mk : ∀ {ι : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_2, u_4} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape ι C],
  (∀ ⦃J : ι → Type w⦄ [inst_2 : (i : ι) → CategoryTheory.SmallCategory (J i)]
      [∀ (i : ι), CategoryTheory.IsFiltered (J i)] ⦃F : (i : ι) → CategoryTheory.Functor (J i) C⦄
      ⦃c : (i : ι) → CategoryTheory.Limits.Cocone (F i)⦄ (a : (i : ι) → CategoryTheory.Limits.IsColimit (c i)),
      Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconePointwiseProduct c))) →
    CategoryTheory.Limits.IsIPCOfShape.{w, u_3, v_2, u_4} ι C
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.mul_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p a b : α},
  Prime p → (FiniteMultiplicity p (a * b) ↔ FiniteMultiplicity p a ∧ FiniteMultiplicity p b)
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map_bot : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), WithZero.map f 0 = 0
-- Mathlib.Data.Fintype.Sets
Set.toFinset_ssubset_toFinset : ∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s.toFinset ⊂ t.toFinset ↔ s ⊂ t
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.diracProbaInverse_eq : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [OpensMeasurableSpace X] [T0Space X] {x : X}
  {μ : ↑(Set.range MeasureTheory.diracProba)}, ↑μ = MeasureTheory.diracProba x → MeasureTheory.diracProbaInverse μ = x
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.op_d : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c) (i j : ι), X.op.d i j = (X.d j i).op
-- Mathlib.Logic.Relation
Relation.TransGen.head'_iff : ∀ {α : Type u_1} {r : α → α → Prop} {a c : α}, Relation.TransGen r a c ↔ ∃ b, r a b ∧ Relation.ReflTransGen r b c
-- Std.Time.Format.Modifier
Std.Time.Modifier.h.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.h presentation = Std.Time.Modifier.h presentation_1 → presentation = presentation_1
-- Init.Data.BitVec.Lemmas
BitVec.toNat_mod_cancel' : ∀ {n : ℕ} {x : BitVec n}, ↑x.toNat % ↑(2 ^ n) = ↑x.toNat