mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSMul.eq_1 : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : SMul M X] [inst_2 : ContinuousConstSMul M X],
  SeparationQuotient.instSMul = { smul := fun c => Quotient.map' (fun x => c • x) ⋯ }
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ico_mem : ∀ {α : Type u_1} [inst : LinearOrder α] (s t : Set α), IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ico l u = S}
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.extendCoordChange_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H},
  (ModelWithCorners.extendCoordChange e e').source = ↑I '' (e.symm.trans e').source
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_compl : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s : Set β} {a : α}, a +ᵥ sᶜ = (a +ᵥ s)ᶜ
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.ext_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B D : LinearMap.BilinForm R M}, B = D ↔ ∀ (x y : M), (B x) y = (D x) y
-- Mathlib.Analysis.Real.Sqrt
NNReal.mul_self_sqrt : ∀ (x : NNReal), NNReal.sqrt x * NNReal.sqrt x = x
-- Mathlib.GroupTheory.IsSubnormal
/-- The intersection of two subnormal subgroups is subnormal.  -/
Subgroup.IsSubnormal.inf : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsSubnormal → K.IsSubnormal → (H ⊓ K).IsSubnormal
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- A basic `ext` lemma for objects of `SimplexCategoryGenRel`.  -/
SimplexCategoryGenRel.ext : ∀ {x y : SimplexCategoryGenRel}, x.len = y.len → x = y
-- Init.Data.Nat.Sqrt.Lemmas
Nat.sqrt_le : ∀ (n : ℕ), n.sqrt * n.sqrt ≤ n
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cochain K L n → Cochain K (L⟦a⟧) n'` when `n' + a = n`.  -/
CochainComplex.HomComplex.Cochain.rightShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          CochainComplex.HomComplex.Cochain K L n →
            (a n' : ℤ) →
              n' + a = n →
                CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
-- Mathlib.Data.Finset.Dedup
List.toFinset_eq_of_perm : ∀ {α : Type u_1} [inst : DecidableEq α] (l l' : List α), l.Perm l' → l.toFinset = l'.toFinset
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsAnd : ∀ {σ : Type u_1} (σs : List (Type u_1)) (P Q₁ Q₂ : σ → Std.Do.SPred σs)
  [base : ∀ (s : σ), Std.Do.SPred.Tactic.IsAnd (P s) (Q₁ s) (Q₂ s)], Std.Do.SPred.Tactic.IsAnd P Q₁ Q₂
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Cofix.bisim_rel : ∀ {F : Type u → Type u} [q : QPF F] (r : QPF.Cofix F → QPF.Cofix F → Prop),
  (∀ (x y : QPF.Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest) → ∀ (x y : QPF.Cofix F), r x y → x = y
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- A morphism version of `le_sup_left`.  -/
CategoryTheory.MonoOver.leSupLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasImages C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        {A : C} → (f g : CategoryTheory.MonoOver A) → f ⟶ (CategoryTheory.MonoOver.sup.obj f).obj g
-- Mathlib.Probability.Independence.Conditional
/-- Two random variables `f, g` are conditionally independent given a third `k` iff the
conditional distribution of `f` given `k` and `g` is equal to the conditional distribution of `f`
given `k`.  -/
ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {γ : Type u_5}
  {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [inst_2 : StandardBorelSpace β]
  [inst_3 : Nonempty β] [StandardBorelSpace β'] [Nonempty β'],
  Measurable f →
    Measurable g →
      ∀ {k : Ω → γ} (hk : Measurable k),
        ProbabilityTheory.CondIndepFun (MeasurableSpace.comap k inferInstance) ⋯ g f μ ↔
          ⇑(ProbabilityTheory.condDistrib f (fun ω => (k ω, g ω))
                μ) =ᵐ[MeasureTheory.Measure.map (fun ω => (k ω, g ω)) μ]
            ⇑(ProbabilityTheory.Kernel.prodMkRight β' (ProbabilityTheory.condDistrib f k μ))
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instGroupWithZero : {K : Type u_5} → [inst : Field K] → {f : Polynomial K} → [Fact (Irreducible f)] → GroupWithZero (AdjoinRoot f)
-- Mathlib.Data.DFinsupp.WellFounded
Function.wellFoundedLT : ∀ {ι : Type u_1} {α : Type u_3} [Finite ι] [inst : Preorder α] [WellFoundedLT α], WellFoundedLT (ι → α)
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.openCell_eq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)),
  Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n ↑i
-- Init.Data.String.Defs
String.byteIdx_endPos : ∀ {s : String}, s.rawEndPos.byteIdx = s.utf8ByteSize
-- Mathlib.Algebra.Lie.Basic
lie_add : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m n : M),
  ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.finallySmall_iff_exists_small_weakly_terminal_set : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFilteredOrEmpty J],
  CategoryTheory.FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
-- Init.Data.String.TakeDrop
/-- Returns the position after the longest prefix of `s` for which `pat` matches
\(potentially repeatedly\).
 -/
String.skipPrefixWhile : {ρ : Type} → (s : String) → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → s.Pos
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instDivOfContinuousDiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Div β]
  [inst_3 : ContinuousDiv β],
  ContinuousMap.instDivOfContinuousDiv = { div := fun f g => { toFun := ⇑f / ⇑g, continuous_toFun := ⋯ } }
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.prod_left_snd : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'}
  {k' : α → G'} {l : Filter α}, Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k' → Asymptotics.IsBigOWith c l g' k'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
/-- This is the general theorem to show that modification operations are correct.  -/
Std.DTreeMap.Internal.Impl.toListModel_updateCell_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced),
  l.Ordered →
    ∀ {k : α} {f : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k)}
      {g : List ((a : α) × β a) → List ((a : α) × β a)},
      (∀ {c : Std.DTreeMap.Internal.Cell α β (compare k)}, (f c).inner.toList = g c.inner.toList) →
        (∀ {l l' : List ((a : α) × β a)}, Std.Internal.List.DistinctKeys l → l.Perm l' → (g l).Perm (g l')) →
          (∀ {l l' : List ((a : α) × β a)}, Std.Internal.List.containsKey k l' = false → g (l ++ l') = g l ++ l') →
            (Std.DTreeMap.Internal.Impl.updateCell k f l hlb).impl.toListModel.Perm (g l.toListModel)
-- Mathlib.Tactic.Linter.UnusedTactic
/-- The unused tactic linter makes sure that every tactic call actually changes *something*.  -/
Mathlib.Linter.linter.unusedTactic : Lean.Option Bool
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_toSet_mk : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (S : Set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S)
  (h₂ : S 0)
  (h₃ :
    ∀ (c : R) {x : M},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier →
        c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier)
  (h₄ :
    ∀ {x : L} {m : M},
      m ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
        ⁅x, m⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier),
  ↑{ carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := h₄ } = S
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.mul : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B₁ B₂ : Set β}
  {f₁ f₂ : α → β} {n : ℕ},
  IsMulFreimanHom n A B₁ f₁ → IsMulFreimanHom n A B₂ f₂ → IsMulFreimanHom n A (B₁ * B₂) (f₁ * f₂)
-- Mathlib.Order.Shrink
instOrderBotShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [inst_1 : Preorder α] → [OrderBot α] → OrderBot (Shrink.{u, u_1} α)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsLittleOTVSIsBigOTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsLittleOTVS 𝕜 l) (Asymptotics.IsBigOTVS 𝕜 l)
                                  (Asymptotics.IsLittleOTVS 𝕜 l)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.add_le_iff_nonpos_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : AddZeroClass α] [AddLeftMono α] {a b : α},
  AddLECancellable a → (a + b ≤ a ↔ b ≤ 0)
-- Mathlib.Topology.CantorBendixson
CantorBendixson.perfectKernel_subset_iteratedDerivedSet : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X) (a : Ordinal.{u}),
  CantorBendixson.perfectKernel s ⊆ CantorBendixson.iteratedDerivedSet s a
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.IsDense.isDenseAt : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  (F : CategoryTheory.Functor C D) [self : F.IsDense] (Y : D), F.isDenseAt Y
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.mk.inj : ∀ {cmdName : String} {wrapper : Lean.Name} {requireProp isInstance : Bool} {cmdName_1 : String} {wrapper_1 : Lean.Name}
  {requireProp_1 isInstance_1 : Bool},
  { cmdName := cmdName, wrapper := wrapper, requireProp := requireProp, isInstance := isInstance } =
      { cmdName := cmdName_1, wrapper := wrapper_1, requireProp := requireProp_1, isInstance := isInstance_1 } →
    cmdName = cmdName_1 ∧ wrapper = wrapper_1 ∧ requireProp = requireProp_1 ∧ isInstance = isInstance_1
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.coneMorphism_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.limit.coneMorphism c).hom = CategoryTheory.Limits.limit.lift F c
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- The data needed to induce a `MonoidalCategory` via the functor `F`; namely, pre-existing
definitions of `⊗`, `𝟙_`, `▷`, `◁` that are preserved by `F`.
 -/
CategoryTheory.Monoidal.InducingFunctorData : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategoryStruct D] → CategoryTheory.Functor D C → Type (max u₂ v₁)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The bi-multiplicative map giving the sign in the Law of Quadratic Reciprocity  -/
qrSign : ℕ → ℕ → ℤ
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CategoryTheory.Functor.commShiftMapCochainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.Additive] → (F.mapHomologicalComplex (ComplexShape.up ℤ)).CommShift ℤ
-- Lean.DocString.Syntax
/-- A list item  -/
Lean.Doc.Syntax.li : Lean.ParserDescr
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `compWithZero h` takes a proof `h` of an equality, inequality, or negation thereof,
and turns it into a proof of a comparison `_ R 0`, where `R ∈ {=, ≤, <}`.
 -/
Mathlib.Tactic.Linarith.compWithZero : Mathlib.Tactic.Linarith.Preprocessor
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_toFormula : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n)
  (v : α ⊕ Fin n → M), φ.toFormula.Realize v ↔ φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
-- Mathlib.Data.Finset.Insert
Finset.insert_subset_insert_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∉ s → (insert a s ⊆ insert a t ↔ s ⊆ t)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instCommMonoidCoeOfSubmonoidClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → CommMonoid (R i)] →
              [∀ (i : ι), SubmonoidClass (S i) (R i)] →
                CommMonoid (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalSubalgebra : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u_3} [inst_1 : UniformSpace A] [CompleteSpace A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : IsSemitopologicalSemiring A] [inst_5 : Module R A]
  [inst_6 : IsScalarTower R A A] [inst_7 : SMulCommClass R A A] [inst_8 : ContinuousConstSMul R A] (x : A),
  CompleteSpace ↥(NonUnitalAlgebra.elemental R x)
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β}, b ∈ t → (fun a => (a, b)) ⁻¹' s ×ˢ t = s
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
/-- The canonical `n`-alternating map from the dual of the `R`-module `M`
to the dual of `⋀[R]^n M`.  -/
exteriorPower.alternatingMapToDual : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (n : ℕ) → Module.Dual R M [⋀^Fin n]→ₗ[R] Module.Dual R ↥(⋀[R]^n M)
-- Mathlib.Data.Num.Basic
/-- Modulus of `ZNum`s.  -/
ZNum.mod : ZNum → ZNum → ZNum
-- Mathlib.Order.Filter.Pointwise
Filter.addCommSemigroup.eq_1 : ∀ {α : Type u_2} [inst : AddCommSemigroup α],
  Filter.addCommSemigroup = { toAddSemigroup := Filter.addSemigroup, add_comm := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflection_apply : ∀ {ι : 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 : ι) (x : M),
  (P.reflection i) x = x - (P.coroot' i) x • P.root i
-- Mathlib.Logic.Equiv.Fin.Basic
Equiv.coe_embeddingFinSucc_symm : ∀ {n : ℕ} {ι : Type u_1} (f : (e : Fin n ↪ ι) × { i // i ∉ Set.range ⇑e }),
  ⇑((Equiv.embeddingFinSucc n ι).symm f) = Fin.cons ↑f.snd ⇑f.fst
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsEmptyCarrierCarrierCommRingCatEmptyCollectionScheme : IsEmpty ↥∅
-- Std.Net.Addr
Std.Net.instInhabitedInterfaceAddress : Inhabited Std.Net.InterfaceAddress
-- Mathlib.Data.Sym.Sym2.Order
Sym2.sup_mk : ∀ {α : Type u_1} [inst : SemilatticeSup α] (a b : α), s(a, b).sup = a ⊔ b
-- Mathlib.RingTheory.Smooth.Kaehler
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`.
Suppose we have a retraction `l` of the injection `I →ₗ[P] S ⊗[P] Ω[P/R]`, then
`x ↦ σ x - l (1 ⊗ D (σ x))` is an algebra homomorphism and a section to `f`,
where `σ` is an arbitrary (set-theoretic) section of `f`
 -/
sectionOfRetractionKerToTensor : {R : Type u_1} →
  {P : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing P] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R P] →
              [inst_4 : Algebra P S] →
                (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) →
                  l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id →
                    [inst_5 : Algebra R S] →
                      [IsScalarTower R P S] →
                        RingHom.ker (algebraMap P S) ^ 2 = ⊥ → Function.Surjective ⇑(algebraMap P S) → S →ₐ[R] P
-- Mathlib.Analysis.Complex.Isometry
/-- The matrix representation of `rotation a` is equal to the conformal matrix
`!![re a, -im a; im a, re a]`.  -/
toMatrix_rotation : ∀ (a : Circle),
  (LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) ↑(rotation a).toLinearEquiv =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_comm : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K ↔ K.IsComplement' H
-- Mathlib.Algebra.Order.Ring.Basic
Even.pow_pos : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Even n → a ≠ 0 → 0 < a ^ n
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.loops_subset_ground : ∀ {α : Type u_1} (M : Matroid α), M.loops ⊆ M.E
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_uniformity_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set (α × α)},
  s ∈ uniformity α ↔ ∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s
-- Mathlib.Algebra.Group.Subgroup.Finite
MonoidHom.fintypeRange.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_3} [inst_1 : Group N] [inst_2 : Fintype G] [inst_3 : DecidableEq N]
  (f : G →* N), f.fintypeRange = Set.fintypeRange ⇑f
-- Mathlib.Data.ENNReal.Inv
ENNReal.mulRightOrderIso_apply : ∀ (a : ENNReal) (ha : IsUnit a) (x : ENNReal), (a.mulRightOrderIso ha) x = x * a
-- Mathlib.Data.ULift
PLift.down_surjective : ∀ {α : Sort u}, Function.Surjective PLift.down
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Swap the two sides of a `BinaryFan`.  -/
CategoryTheory.Limits.BinaryFan.swap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Limits.BinaryFan X Y → CategoryTheory.Limits.BinaryFan Y X
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_one : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : One β], ↑1 =ᵐ[μ] 1
-- Mathlib.Tactic.Translate.ToDual
/-- Dictionary used by `guessName` to autogenerate names.
This only transforms single name components, unlike `abbreviationDict`.

Note: `guessName` capitalizes the output according to the capitalization of the input.
In order for this to work, the input should always start with a lower case letter, and the output
should always start with an upper case letter.
 -/
Mathlib.Tactic.ToDual.nameDict : Std.HashMap String (List String)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsCycle.cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α},
  σ.IsCycle → σ.cycleType = {σ.support.card}
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
_private.Mathlib.Topology.UniformSpace.UniformConvergenceTopology.0.UniformFun.«term𝒰(_,_,_)» : Lean.ParserDescr
-- Mathlib.Data.List.InsertIdx
/-- Erasing an index commutes with `List.map`.  -/
List.eraseIdx_map : ∀ {α : Type u} {β : Type v} (f : α → β) (l : List α) (n : ℕ), (List.map f l).eraseIdx n = List.map f (l.eraseIdx n)
-- Mathlib.Data.Part
Part.inter_get_eq : ∀ {α : Type u_1} [inst : Inter α] (a b : Part α) (hab : (a ∩ b).Dom), (a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eq_head?_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
    Std.Internal.List.minKey? l = (Std.Internal.List.keys l).head?
-- Mathlib.NumberTheory.Divisors
Nat.ne_zero_of_mem_divisors : ∀ {n m : ℕ}, n ∈ m.divisors → m ≠ 0
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.of_free : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  Module.Flat R M
-- Std.Sync.Broadcast
Std.Broadcast.Error.closed.sizeOf_spec : sizeOf Std.Broadcast.Error.closed = 1
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrLeft_sumInl : ∀ {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι'' → Type u_9) (e : ι ⊕ ι' ≃ ι'')
  (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (i : ι),
  (Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun x => π (e x)).symm (f, g)) (e (Sum.inl i)) = f i
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.μ_iso_of_reflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective R],
  CategoryTheory.IsIso (CategoryTheory.reflectorAdjunction R).toMonad.μ
-- Mathlib.Data.Nat.Bitwise
Nat.lt_xor_cases : ∀ {a b c : ℕ}, a < b ^^^ c → a ^^^ c < b ∨ a ^^^ b < c
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.lineDerivOpCLM.congr_simp : ∀ (R : Type u_4) {V : Type u_5} (E : Type u_6) {F : Type u_7} [inst : Ring R] [inst_1 : AddCommGroup E]
  [inst_2 : Module R E] [inst_3 : AddCommGroup F] [inst_4 : Module R F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup V] [inst_8 : LineDeriv V E F] [inst_9 : LineDerivAdd V E F]
  [inst_10 : LineDerivSMul R V E F] [inst_11 : ContinuousLineDeriv V E F] (m m_1 : V),
  m = m_1 → LineDeriv.lineDerivOpCLM R E m = LineDeriv.lineDerivOpCLM R E m_1
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instOne.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α], LowerSet.instOne = { one := LowerSet.Iic 1 }
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_40 : HAdd Std.Time.Week.Offset Std.Time.Hour.Offset Std.Time.Hour.Offset
-- Init.Data.Vector.Find
Vector.find?_append : ∀ {α : Type} {n₁ n₂ : ℕ} {p : α → Bool} {xs : Vector α n₁} {ys : Vector α n₂},
  Vector.find? p (xs ++ ys) = (Vector.find? p xs).or (Vector.find? p ys)
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.cauchy_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_u : UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible]
  {F : Filter R},
  Cauchy F ↔
    F.NeBot ∧ ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
-- Mathlib.Tactic.Bound
/-- Aesop configuration for `bound`  -/
Mathlib.Tactic.Bound.boundConfig : Aesop.Options
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_unitOfList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.DTreeMap.Raw.Const.unitOfList l cmp).size ≤ l.length
-- Init.Data.Subtype.Order
Subtype.instIsPartialOrder : ∀ {α : Type u} [inst : LE α] [Std.IsPartialOrder α] {P : α → Prop}, Std.IsPartialOrder (Subtype P)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.mk : Lean.PHashMap Lean.Meta.Origin ℕ → ℕ → Lean.Meta.Simp.UsedSimps