mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.reverse_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.map f p).reverse = SimpleGraph.Walk.map f p.reverse
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k a : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getKey! a = if compare k a = Ordering.eq then default else t.getKey! a
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_eq_sum : ∀ {ι : Type u_2} [inst : Fintype ι] {p : ENNReal} [inst_1 : Fact (1 ≤ p)] {β : ι → Type u_5},
  p ≠ ⊤ →
    ∀ [inst_2 : (i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp p β),
      ‖f‖₊ = (∑ i, ‖f.ofLp i‖₊ ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.RingTheory.Multiplicity
emultiplicity_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p a b : α},
  Prime p → emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Pos.find?_eq_find?_toSlice : ∀ {ρ : Type} {pat : ρ} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String} {p : s.Pos}, p.find? pat = Option.map String.Pos.ofToSlice (p.toSlice.find? pat)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (t.truncGEπ n) (t.truncGEδLT n) = 0
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- Exterior derivative commutes with pullback.  -/
extDeriv_pullback : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} {r : WithTop ℕ∞} {x : E}
  {ω : F → F [⋀^Fin n]→L[𝕜] G} {f : E → F},
  DifferentiableAt 𝕜 ω (f x) →
    ContDiffAt 𝕜 r f x →
      minSmoothness 𝕜 2 ≤ r →
        extDeriv (fun x => (ω (f x)).compContinuousLinearMap (fderiv 𝕜 f x)) x =
          (extDeriv ω (f x)).compContinuousLinearMap (fderiv 𝕜 f x)
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- A linear equivalence of two modules restricts to a linear equivalence from the preimage of any
submodule to that submodule.

This is `LinearEquiv.ofSubmodule` but with `comap` on the left instead of `map` on the right.  -/
LinearEquiv.ofSubmodule' : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {σ₁₂ : R →+* R₂} →
                  {σ₂₁ : R₂ →+* R} →
                    {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                      {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                        [inst_4 : Module R M] →
                          [inst_5 : Module R₂ M₂] →
                            (f : M ≃ₛₗ[σ₁₂] M₂) → (U : Submodule R₂ M₂) → ↥(Submodule.comap (↑f) U) ≃ₛₗ[σ₁₂] ↥U
-- Std.Data.ExtHashMap.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtHashMap.getKey : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [inst : EquivBEq α] → [inst_1 : LawfulHashable α] → (m : Std.ExtHashMap α β) → (a : α) → a ∈ m → α
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_ne_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {y : P}, FractionalIdeal.spanSingleton S y ≠ 0 ↔ y ≠ 0
-- Mathlib.Topology.DerivedSet
/-- In a `T1Space`, the `derivedSet` of the closure of a set is equal to the derived set of the
set itself.

Note: this doesn't hold in a space with the indiscrete topology. For example, if `X` is a type with
two elements, `x` and `y`, and `A := {x}`, then `closure A = Set.univ` and `derivedSet A = {y}`,
but `derivedSet Set.univ = Set.univ`.  -/
derivedSet_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] (A : Set X), derivedSet (closure A) = derivedSet A
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.HomologyMapData.map_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂}
  {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h₁.left.IsPreservedBy F]
  [inst_6 : h₁.right.IsPreservedBy F] [inst_7 : h₂.left.IsPreservedBy F] [inst_8 : h₂.right.IsPreservedBy F],
  (ψ.map F).left = ψ.left.map F
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.mono : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G} {A' B' : Finset G},
  A ⊆ A' → B ⊆ B' → UniqueMul A' B' a0 b0 → UniqueMul A B a0 b0
-- Batteries.Recycling.RBTree.WF
/-- `O(n)`. Map a function on the values in the map.  -/
RBTree.RBMap.mapVal : {α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → {cmp : α → α → Ordering} → (α → β → γ) → RBTree.RBMap α β cmp → RBTree.RBMap α γ cmp
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- Let `A', A, B', B` be subgroups of `G`. If `A' ≤ B'` and `A ≤ B`,
then there is a map `A / (A' ⊓ A) →* B / (B' ⊓ B)` induced by the inclusions.  -/
QuotientGroup.quotientMapSubgroupOfOfLe : {G : Type u} →
  [inst : Group G] →
    {A' A B' B : Subgroup G} →
      [_hAN : (A'.subgroupOf A).Normal] →
        [_hBN : (B'.subgroupOf B).Normal] → A' ≤ B' → A ≤ B → ↥A ⧸ A'.subgroupOf A →* ↥B ⧸ B'.subgroupOf B
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_def : ∀ (a b : ℤ), a % b = a - b * (a / b)
-- Mathlib.Computability.Primrec.Basic
Primrec.list_getElem?₁ : ∀ {α : Type u_1} [inst : Primcodable α] (l : List α), Primrec fun x => l[x]?
-- Init.Data.List.Range
/-- Replace `zipIdx` with a starting index `n+1` with `zipIdx` starting from `n`,
followed by a `map` increasing the indices by one.  -/
List.zipIdx_succ : ∀ {α : Type u_1} {l : List α} {i : ℕ},
  l.zipIdx (i + 1) =
    List.map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      (l.zipIdx i)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zpow_eq_one_iff_dvd : ∀ {G : Type u_3} [inst : DivisionCommMonoid G] {k : ℕ} {ζ : G}, IsPrimitiveRoot ζ k → ∀ (l : ℤ), ζ ^ l = 1 ↔ ↑k ∣ l
-- Mathlib.RingTheory.Trace.Basic
Algebra.embeddingsMatrix.eq_1 : ∀ {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : CommRing C] [inst_4 : Algebra A C] (b : κ → B),
  Algebra.embeddingsMatrix A C b = Matrix.of fun i σ => σ (b i)
-- Init.Data.UInt.Lemmas
UInt32.neg_one_eq : -1 = 4294967295
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_map_left_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.toArrowArrowFunctor'.map φ).left.right = φ.τ₂
-- Init.Data.List.Basic
/-- The base case: `[]` is a sublist of `[]`  -/
List.Sublist.slnil : ∀ {α : Type u_1}, [].Sublist []
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantFrom i₀ →
    ∀ [CategoryTheory.IsFiltered J] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c),
      CategoryTheory.IsIso (c.ι.app i₀)
-- Init.Data.BitVec.Lemmas
BitVec.not_concat : ∀ {w : ℕ} (x : BitVec w) (b : Bool), ~~~x.concat b = (~~~x).concat !b
-- Mathlib.RingTheory.OreLocalization.OreSet
/-- **Alias** of `OreLocalization.oreSetOfIsCancelMulZero`.

---

Cancellability in monoids with zeros can act as a replacement for the `ore_right_cancel`
condition of an ore set.  -/
OreLocalization.oreSetOfCancelMonoidWithZero : {R : Type u_1} →
  [inst : MonoidWithZero R] →
    [IsCancelMulZero R] →
      {S : Submonoid R} →
        (oreNum : R → ↥S → R) →
          (oreDenom : R → ↥S → ↥S) →
            (∀ (r : R) (s : ↥S), ↑(oreDenom r s) * r = oreNum r s * ↑s) → OreLocalization.OreSet S
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Hall-Witt identity**  -/
conj_commutatorElement_left_commutatorElement_mul : ∀ {G : Type u_1} [inst : Group G] (a b c : G),
  a * ⁅⁅a⁻¹, b⁆, c⁆ * a⁻¹ * c * ⁅⁅c⁻¹, a⁆, b⁆ * c⁻¹ * b * ⁅⁅b⁻¹, c⁆, a⁆ * b⁻¹ = 1
-- Mathlib.Algebra.Homology.Homotopy
prevD_comp_right : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : (i j : ι) → C.X i ⟶ D.X j) (g : D ⟶ E) (j : ι),
  ((prevD j) fun i j => CategoryTheory.CategoryStruct.comp (f i j) (g.f j)) =
    CategoryTheory.CategoryStruct.comp ((prevD j) f) (g.f j)
-- Mathlib.Order.RelSeries
SetRel.IsWellFounded.of_finiteDimensional : ∀ {α : Type u_1} (r : SetRel α α) [r.FiniteDimensional], r.IsWellFounded
-- Mathlib.Topology.Path
Path.toContinuousMap : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → Path x y → C(↑unitInterval, X)
-- Mathlib.Tactic.CancelDenoms.Core
/-- Helper lemma to chain together two `simp` proofs and the result of `mkProdPrf`.  -/
Mathlib.Tactic.CancelDenoms.derive_trans₂ : ∀ {α : Type u_1} [inst : Mul α] {a b c d e : α}, a = b → b = c → d * c = e → d * a = e
-- Mathlib.RingTheory.FiniteType
/-- An element of `R[M]` is in the subalgebra generated by its support.  -/
MonoidAlgebra.mem_adjoin_support : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Monoid M] (f : MonoidAlgebra R M),
  f ∈ Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ↑f.coeff.support)
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.dvd_C_iff_exists : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R] {f : MvPolynomial σ R} {a : R},
  a ≠ 0 → (f ∣ MvPolynomial.C a ↔ ∃ b, b ∣ a ∧ f = MvPolynomial.C b)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_option : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : Option ι → V},
  LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ v none ∉ Submodule.span K (Set.range (v ∘ some))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cocycle K L n → Cocycle (K⟦a⟧) L n'` when `n + a = n'`.  -/
CochainComplex.HomComplex.Cocycle.leftShift : {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' : ℤ) →
              n + a = n' →
                CochainComplex.HomComplex.Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
-- Mathlib.Topology.LocallyFinsupp
/-- **Alias** of `Function.locallyFinsuppWithin.mk_of_mem_addSubgroup`.

---

Assign a function with locally finite support within `U` to a function in the subgroup.
 -/
Function.locallyFinsuppWithin.mk_of_mem : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} →
      {Y : Type u_2} →
        [inst_1 : AddGroup Y] →
          (f : X → Y) → f ∈ Function.locallyFinsuppWithin.addSubgroup U → Function.locallyFinsuppWithin U Y
-- Init.Data.Array.FinRange
Array.finRange_reverse : ∀ {n : ℕ}, (Array.finRange n).reverse = Array.map Fin.rev (Array.finRange n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km fallback : α}, t.maxKey? = some km → t.getKeyD km fallback = km
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.coe_mulRight₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MeasurableSpace G₀] [inst_2 : MeasurableMul G₀] {g : G₀}
  (hg : g ≠ 0), ⇑(MeasurableEquiv.mulRight₀ g hg) = fun x => x * g
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.precompHomeomorph_symm_apply : ∀ {R A B : CommRingCat} [inst : TopologicalSpace ↑R] (f : A ≅ B) (φ : A ⟶ R),
  (CommRingCat.HomTopology.precompHomeomorph f).symm φ = CategoryTheory.CategoryStruct.comp f.inv φ
-- Mathlib.Data.List.GetD
List.getI_eq_default : ∀ {α : Type u} (l : List α) [inst : Inhabited α] {n : ℕ}, l.length ≤ n → l.getI n = default
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Module.Basis.equivFunL_apply : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E]
  [inst_5 : CompleteSpace 𝕜] {ι : Type u_1} [inst_6 : Finite ι] [inst_7 : T2Space E] (v : Module.Basis ι 𝕜 E) (x : E)
  (a : ι), v.equivFunL x a = (v.repr x) a
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.curryRingEquiv_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N] (m : M)
  (n : N) (r : R),
  AddMonoidAlgebra.curryRingEquiv (AddMonoidAlgebra.single (m, n) r) =
    AddMonoidAlgebra.single m (AddMonoidAlgebra.single n r)
-- Batteries.Data.MLList.Basic
/-- Apply a function returning values inside the monad to a monadic lazy list,
returning only the first successful result.
 -/
MLList.firstM : {m : Type u_1 → Type u_1} → {α β : Type u_1} → [AlternativeMonad m] → MLList m α → (α → m (Option β)) → m β
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.coneOfConeForget_π_app : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) (j : J),
  (TopCat.coneOfConeForget c).π.app j =
    TopCat.ofHom { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (c.π.app j)), continuous_toFun := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_union_of_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The initial object in `Type u` is `PEmpty`.  -/
CategoryTheory.Limits.Types.isInitialPEmpty : CategoryTheory.Limits.IsInitial PEmpty.{u + 1}
-- Mathlib.Order.Ideal
/-- The `Cofinal` contains arbitrarily large elements.  -/
Order.Cofinal.isCofinal : ∀ {P : Type u_2} [inst : Preorder P] (self : Order.Cofinal P), IsCofinal self.carrier
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.any_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α]
  [EquivBEq α] {p : α → Bool}, m.WF → m.keys.any p = m.any fun a x => p a
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyFaithful.jointlyReflectEpimorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyFaithful F → CategoryTheory.JointlyReflectEpimorphisms F
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.not_mem_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α},
  a ∉ ∅
-- Mathlib.Algebra.Order.Kleene
/-- An idempotent semiring is a semiring with the additional property that addition is idempotent.
 -/
IdemSemiring : Type u_5 → Type u_5
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S')
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T} (f_1 : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.map f).map f_1).right = f_1.right
-- Init.Control.Option
/-- A recoverable failure.
 -/
OptionT.fail : {m : Type u → Type v} → [Monad m] → {α : Type u} → OptionT m α
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_apply_module' : ∀ {k : Type u_1} {V1 : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] (p₀ p₁ : V1) (c : k),
  (AffineMap.lineMap p₀ p₁) c = c • (p₁ - p₀) + p₀
-- Mathlib.Data.Erased
Erased.instRepr : (α : Type u) → Repr (Erased α)
-- Init.Data.Nat.Fold
Nat.any_eq_finRange_any : ∀ {n : ℕ} (f : (i : ℕ) → i < n → Bool),
  n.any f =
    (List.finRange n).any fun x =>
      match x with
      | ⟨i, h⟩ => f i h
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.enrichedOrdinaryCategory : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.EnrichedCategory V D] →
          CategoryTheory.EnrichedOrdinaryCategory V (CategoryTheory.ForgetEnrichment V D)
-- Mathlib.Topology.FiberBundle.Constructions
Pullback.TotalSpace.topologicalSpace.eq_1 : ∀ {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} (f : B' → B) [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)],
  Pullback.TotalSpace.topologicalSpace F E f = pullbackTopology F E f
-- Mathlib.Topology.Constructions
nhds_toMul : ∀ {X : Type u} [inst : TopologicalSpace X] (x : Additive X),
  nhds (Additive.toMul x) = Filter.map (⇑Additive.toMul) (nhds x)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.isPartitionTop : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), ⊤.IsPartition
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instInv.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Inv Y],
  LocallyConstant.instInv = { inv := fun f => { toFun := (⇑f)⁻¹, isLocallyConstant := ⋯ } }
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- A null set has empty interior.  -/
MeasureTheory.Measure.interior_eq_empty_of_null : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {s : Set X}, μ s = 0 → interior s = ∅
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, then the distance from
`f n` to the limit of `f` is bounded above by `C * r^n / (1 - r)`.  -/
edist_le_of_edist_le_geometric_of_tendsto : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (r C : ENNReal) {f : ℕ → α},
  (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), edist (f n) a ≤ C * r ^ n / (1 - r)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.norm_eval_le_injectiveSeminorm : ∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_1}
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] (f : ContinuousMultilinearMap 𝕜 E F)
  (x : PiTensorProduct 𝕜 fun i => E i),
  ‖(PiTensorProduct.lift f.toMultilinearMap) x‖ ≤ ‖f‖ * PiTensorProduct.injectiveSeminorm x
-- Lean.Elab.Tactic.Basic
/-- Add the given goals at the end of the current list of goals.  -/
Lean.Elab.Tactic.appendGoals : List Lean.MVarId → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.fst_eq_fst' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y Z : CategoryTheory.Over X),
  CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z = CategoryTheory.ChosenPullbacksAlong.fst' Y.hom Z.hom
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- If a `Fan` is limit, then its opposite is colimit.  -/
CategoryTheory.Limits.Fan.IsLimit.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} →
      {Z : α → C} →
        {f : CategoryTheory.Limits.Fan Z} → CategoryTheory.Limits.IsLimit f → CategoryTheory.Limits.IsColimit f.op
-- Init.Data.List.Lemmas
List.not_all_eq_any_not : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, (!l.all p) = l.any fun a => !p a
-- Lean.Elab.App
/-- The type of `f` once loose bvars are instantiated with `fArgs`, reduced to WHNF if it is a forall
after `fTypeIsForall` is called.  -/
Lean.Elab.Term.ElabAppArgs.State.fType : Lean.Elab.Term.ElabAppArgs.State → Lean.Expr
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
ConformalAt.differentiableAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y] [inst_2 : NormedSpace ℝ X]
  [inst_3 : NormedSpace ℝ Y] {f : X → Y} {x : X}, ConformalAt f x → DifferentiableAt ℝ f x
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.instCoeQuotientSubgroup : {α : Type u_1} → [inst : Group α] → {s : Subgroup α} → Coe α (α ⧸ s)
-- Mathlib.Analysis.Convex.Strict
Set.Subsingleton.strictConvex : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommMonoid E] [inst_4 : Module 𝕜 E] {s : Set E}, s.Subsingleton → StrictConvex 𝕜 s
-- Mathlib.Algebra.BigOperators.Finprod
/-- If the multiplicative supports of `f` and `g` are finite, then the product of `f i / g i`
equals the product of `f i` divided by the product of `g i`.  -/
finprod_div_distrib : ∀ {α : Type u_1} {G : Type u_4} [inst : DivisionCommMonoid G] {f g : α → G},
  Function.HasFiniteMulSupport f →
    Function.HasFiniteMulSupport g → ∏ᶠ (i : α), f i / g i = (∏ᶠ (i : α), f i) / ∏ᶠ (i : α), g i
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_iff_neg_mem : ∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Convex ℝ s → (Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinitaryCardAugment_finitary : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug :
    ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact
        subset_ground).matroid.Finitary
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.eraseManyEntries_impl_perm_eraseList : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {t₁ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF) {t₂ : Std.DTreeMap.Internal.Impl α β},
  (↑(t₁.eraseManyEntries t₂ ⋯)).toListModel.Perm
    (Std.Internal.List.eraseList t₁.toListModel (List.map (fun x => x.fst) t₂.toListModel))
-- Mathlib.Order.Hom.Lattice
SupHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : SupHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_sup' := ⋯ }