mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.CommRingCat.Colimits.descFunLift.match_1.eq_1 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (motive : CommRingCat.Colimits.Prequotient F → Sort u_2) (j : J) (x : ↑(F.obj j))
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (CommRingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive CommRingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive CommRingCat.Colimits.Prequotient.one)
  (h_4 : (x : CommRingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match CommRingCat.Colimits.Prequotient.of j x with
    | CommRingCat.Colimits.Prequotient.of j x => h_1 j x
    | CommRingCat.Colimits.Prequotient.zero => h_2 ()
    | CommRingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_1 j x
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_emptyOn : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (Matroid.emptyOn β).comap f = Matroid.emptyOn α
-- Mathlib.Data.List.Destutter
List.destutter_idem : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R],
  List.destutter R (List.destutter R l) = List.destutter R l
-- Init.Data.String.Iterate
String.instForInCharOfMonad : {m : Type u → Type v} → [Monad m] → ForIn m String Char
-- Lean.Expr
Lean.ExprStructEq.mk.inj : ∀ {val val_1 : Lean.Expr}, { val := val } = { val := val_1 } → val = val_1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instInhabitedK' : Inhabited Turing.PartrecToTM2.K'
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves colimits, then `F.rightOp : C ⥤ Dᵒᵖ` preserves limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp
-- Mathlib.Topology.ContinuousMap.Ideals
/-- An auxiliary lemma used in the proof of `ContinuousMap.idealOfSet_ofIdeal_eq_closure` which may
be useful on its own.  -/
ContinuousMap.exists_mul_le_one_eqOn_ge : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f : C(X, NNReal)) {c : NNReal},
  0 < c → ∃ g, (∀ (x : X), (g * f) x ≤ 1) ∧ Set.EqOn (⇑(g * f)) 1 {x | c ≤ f x}
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.powFn? : Lean.Meta.Sym.Arith.Ring → Option Lean.Expr
-- Aesop.RuleTac.Basic
Aesop.RuleTac.ofSingleRuleTac : Aesop.SingleRuleTac → Aesop.RuleTac
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Recursive implementation for `withExistsElimAlongPath`.  -/
ExistsAndEq.withExistsElimAlongPathImp : {u : Lean.Level} →
  {α : Q(Sort u)} →
    {P goal : Q(Prop)} →
      Q(«$P») →
        {a a' : Q(«$α»)} →
          List ExistsAndEq.VarQ →
            ExistsAndEq.Path →
              List ExistsAndEq.HypQ →
                (Q(«$a» = «$a'») → List ExistsAndEq.HypQ → Lean.MetaM Q(«$goal»)) → Lean.MetaM Q(«$goal»)
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Finset.mulSupport_prod : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → κ → M),
  (Function.mulSupport fun x => ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.mulSupport (f i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α] {f : (a : α) → β a → γ a}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = Std.Internal.List.getKey? k l
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instIsDomainOfIsCancelAdd : ∀ {R : Type u} [inst : Semiring R] [IsCancelAdd R] [IsDomain R], IsDomain (Polynomial R)
-- Init.Prelude
Or.neg_resolve_left : ∀ {a b : Prop}, ¬a ∨ b → a → b
-- Mathlib.Topology.UniformSpace.Equiv
/-- `α × {*}` is uniformly isomorphic to `α`.  -/
UniformEquiv.prodPUnit : (α : Type u) → [inst : UniformSpace α] → α × PUnit.{u_4 + 1} ≃ᵤ α
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mapAlgHom_comp_mapAlghom : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing T] [inst_3 : CommRing U] [inst_4 : Algebra R S] [inst_5 : Algebra R T] [inst_6 : Algebra R U]
  (f : S →ₐ[R] T) (g : T →ₐ[R] U) (p : Polynomial S) (q : Polynomial T) (r : Polynomial U)
  (hf : q ∣ Polynomial.map (↑f) p) (hg : r ∣ Polynomial.map (↑g) q),
  (AdjoinRoot.mapAlgHom g q r hg).comp (AdjoinRoot.mapAlgHom f p q hf) = AdjoinRoot.mapAlgHom (g.comp f) p r ⋯
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.sub_eq_add_neg : ∀ (xs ys : Lean.Omega.Coeffs), xs - ys = xs + -ys
-- Lean.Parser.Types
Lean.Parser.Parser.mk : Lean.Parser.ParserInfo → Lean.Parser.ParserFn → Lean.Parser.Parser
-- Mathlib.Analysis.Calculus.Deriv.Abs
differentiableOn_abs : ∀ {s : Set ℝ}, (∀ x ∈ s, x ≠ 0) → DifferentiableOn ℝ (fun x => |x|) s
-- Lean.Parser.Basic
Lean.Parser.isIdCont : Lean.Parser.ParserContext → Lean.Parser.ParserState → Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.OLeanEntry.mk.sizeOf_spec : ∀ (key : Lean.KeyedDeclsAttribute.Key) (declName : Lean.Name),
  sizeOf { key := key, declName := declName } = 1 + sizeOf key + sizeOf declName
-- Mathlib.GroupTheory.Commutator.Basic
map_addCommutator_eq : ∀ (G : Type u_1) [inst : AddGroup G] {H : Type u_4} [inst_1 : AddGroup H] (f : G →+ H),
  AddSubgroup.map f (addCommutator G) = ⁅f.range, f.range⁆
-- Mathlib.Order.Filter.Pointwise
Filter.addZeroClass.eq_1 : ∀ {α : Type u_2} [inst : AddZeroClass α],
  Filter.addZeroClass = { toZero := Filter.instZero, toAdd := Filter.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget_createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommMonCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] →
        CategoryTheory.CreatesLimit F (CategoryTheory.forget AddCommMonCat)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.Braided.instId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.Functor.id C).Braided
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- Eta-expanded form of `meromorphicTrailingCoeffAt_comp_sub_const_eq_meromorphicTrailingCoeffAt`

---

`meromorphicTrailingCoefficientAt` is invariant under translation.  -/
meromorphicTrailingCoeffAt_fun_comp_sub_const_eq_meromorphicTrailingCoeffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x c : 𝕜},
  meromorphicTrailingCoeffAt (fun x => f (x - c)) x = meromorphicTrailingCoeffAt f (x - c)
-- Mathlib.Data.FinEnum
FinEnum.mem_toList : ∀ {α : Type u} [inst : FinEnum α] (x : α), x ∈ FinEnum.toList α
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `insertIfNew` which can be used in the absence of balance
information but still assumes the preconditions of `insertIfNew`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.insertIfNew! : {α : Type u} →
  {β : α → Type v} → [Ord α] → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Definable.out_equiv : ∀ {n : ℕ} (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) [inst : ZFSet.Definable n f] {xs ys : Fin n → PSet.{u}},
  (∀ (i : Fin n), xs i ≈ ys i) → ZFSet.Definable.out f xs ≈ ZFSet.Definable.out f ys
-- Mathlib.Topology.MetricSpace.ProperSpace
instSecondCountableTopologyReal : SecondCountableTopology ℝ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_mono : ∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph}, H ≤ H' → H.verts ⊆ H'.verts
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Sum of elements in a `NonUnitalSubring` of a `NonUnitalRing` indexed by a `Finset`
is in the `NonUnitalSubring`.  -/
NonUnitalSubring.sum_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {ι : Type u_2} {t : Finset ι} {f : ι → R},
  (∀ c ∈ t, f c ∈ s) → ∑ i ∈ t, f i ∈ s
-- Mathlib.Data.Setoid.Partition
/-- The projection onto the quotient associated to an indexed partition.  -/
IndexedPartition.proj : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → (hs : IndexedPartition s) → α → hs.Quotient
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedHull_add_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E}
  [NormOneClass 𝕜] {t : Set E}, balancedHull 𝕜 (s + t) ⊆ balancedHull 𝕜 s + balancedHull 𝕜 t
-- Batteries.Data.String.Lemmas
String.length_eq_of_map_eq : ∀ {a b : String} {f g : Char → Char}, String.map f a = String.map g b → a.length = b.length
-- Mathlib.Topology.Homeomorph.Lemmas
Fin.appendHomeomorph_symm_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] (m n : ℕ) (f : Fin (m + n) → X),
  (Fin.appendHomeomorph m n).symm f = (fun i => f (Fin.castAdd n i), fun i => f (Fin.natAdd m i))
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δ_eq : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : Q.toExtension.H1Cotangent)
  (y : (Q.comp P).toExtension.Cotangent),
  (Algebra.Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x →
    ∀ (z : TensorProduct S T P.toExtension.CotangentSpace),
      (LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
          (Q.comp P).toExtension.cotangentComplex y →
        (Algebra.Generators.H1Cotangent.δ Q P) x = (LinearMap.baseChange T P.toExtension.toKaehler) z
-- Mathlib.Analysis.BoxIntegral.Integrability
/-- The indicator function of a measurable set is McShane integrable with respect to any
locally-finite measure.  -/
BoxIntegral.hasIntegralIndicatorConst : ∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (l : BoxIntegral.IntegrationParams),
  l.bRiemann = false →
    ∀ {s : Set (ι → ℝ)},
      MeasurableSet s →
        ∀ (I : BoxIntegral.Box ι) (y : E) (μ : MeasureTheory.Measure (ι → ℝ))
          [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
          BoxIntegral.HasIntegral I l (s.indicator fun x => y) μ.toBoxAdditive.toSMul (μ.real (s ∩ ↑I) • y)
-- Mathlib.Algebra.Quotient
/-- Quotient notation based on the `HasQuotient` typeclass  -/
«term_⧸_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atBot_iSup : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : CompleteLattice α]
  [SupConvergenceClass α] {f : ι → α}, Antitone f → Filter.Tendsto f Filter.atBot (nhds (⨆ i, f i))
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix'_toLinearMapₛₗ₂' : ∀ {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m]
  (M : Matrix n m N₂), (LinearMap.toMatrixₛₗ₂' R) ((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) = M
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.Value.mk.sizeOf_spec : ∀ (n : ℕ) (value : Fin n), sizeOf { n := n, value := value } = 1 + sizeOf n + sizeOf value
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map_id : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal]
  (h : optParam (N ≤ Subgroup.comap (MonoidHom.id G) N) ⋯),
  QuotientGroup.map N N (MonoidHom.id G) h = MonoidHom.id (G ⧸ N)
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.semiringInst : Lean.Meta.Grind.Arith.FieldNormNum.Context✝ → Lean.Expr
-- Mathlib.Analysis.Convex.StdSimplex
/-- All values of a function `f ∈ stdSimplex 𝕜 ι` belong to `[0, 1]`.  -/
mem_Icc_of_mem_stdSimplex : ∀ {𝕜 : Type u_2} {ι : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι]
  [IsOrderedAddMonoid 𝕜] {f : ι → 𝕜}, f ∈ stdSimplex 𝕜 ι → ∀ (x : ι), f x ∈ Set.Icc 0 1
-- Mathlib.FieldTheory.IsAlgClosed.Classification
/-- If `K` is an uncountable algebraically closed field, then its
cardinality is the same as that of a transcendence basis.

For a simpler, but less universe-polymorphic statement, see
`IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'`  -/
IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt : ∀ {R : Type u} {K : Type v} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsAlgClosed K] {ι : Type w}
  (v : ι → K) [Nontrivial R],
  IsTranscendenceBasis R v →
    Cardinal.mk R ≤ Cardinal.aleph0 →
      Cardinal.aleph0 < Cardinal.mk K → Cardinal.lift.{w, v} (Cardinal.mk K) = Cardinal.lift.{v, w} (Cardinal.mk ι)
-- Mathlib.Data.Set.Function
Set.LeftInvOn.image_inter' : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β} {f' : β → α},
  Set.LeftInvOn f' f s → f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s
-- Mathlib.Data.Seq.Computation
Computation.ret_bind : ∀ {α : Type u} {β : Type v} (a : α) (f : α → Computation β), (Computation.pure a).bind f = f a
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.toRingEquiv_symm_uniqueAlgEquiv : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] [inst_4 : Unique M],
  ↑(AddMonoidAlgebra.uniqueAlgEquiv R M).symm = (AddMonoidAlgebra.uniqueRingEquiv M).symm
-- Mathlib.RingTheory.Adjoin.Singleton
Algebra.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C]
  [inst_6 : IsScalarTower A B C] (b : B), IsScalarTower (↥A[b]) (↥A[(algebraMap B C) b]) C
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A copy gives rise to an embedding of vertex types.  -/
SimpleGraph.Copy.toEmbedding : {α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → A.Copy B → α ↪ β
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn'_congr : ∀ {γ α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] [Monad m]
  [inst_2 : Std.Iterator α m β] [inst_3 : Std.IteratorLoop α m n] [inst_4 : MonadLiftT m n] {ita itb : Std.IterM m β}
  (w : ita = itb) {b b' : γ},
  b = b' →
    ∀ {f : (a' : β) → a' ∈ ita → γ → n (ForInStep γ)} {g : (a' : β) → a' ∈ itb → γ → n (ForInStep γ)},
      (∀ (a : β) (m_1 : a ∈ itb) (b : γ), f a ⋯ b = g a m_1 b) → forIn' ita b f = forIn' itb b' g
-- Mathlib.Topology.List
instTopologicalSpaceList : {α : Type u_1} → [TopologicalSpace α] → TopologicalSpace (List α)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyIsoSc'_hom_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom
      (CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι h) =
    CategoryTheory.CategoryStruct.comp (K.homologyι j)
      (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).hom h)
-- Mathlib.NumberTheory.NumberField.AdeleRing
NumberField.instTopologicalSpaceAdeleRing : (R : Type u_1) →
  (K : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : IsDedekindDomain R] →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → TopologicalSpace (NumberField.AdeleRing R K)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableOn.neg` -/
DifferentiableOn.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (fun i => -f i) s
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseKey_cons_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'},
  (k' == k) = true → Std.Internal.List.eraseKey k (⟨k', v'⟩ :: l) = l
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_bot : ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M},
  x ∈ ⊥ ↔ x = 0
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C),
  CategoryTheory.Limits.colimitHomIsoLimitYoneda F A = CategoryTheory.Limits.colimitHomIsoLimitYoneda F A
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_smul : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : List α) (b : β), FreeMonoid.ofList l • b = List.foldr f b l
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_zero : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] [Nontrivial n],
  Matrix.cramer 0 = 0
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.eq_1 : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂), f.HasNoetherianRange = IsNoetherian K ↥f.range
-- Mathlib.LinearAlgebra.SModEq.Pointwise
/-- A variant of `SModEq.smul`, where the scalar belongs to an ideal.
 -/
SModEq.smul' : ∀ {R : Type u_1} [inst : Ring R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {U : Submodule R M} {x y : M}, x ≡ y [SMOD U] → ∀ {c : R}, c ∈ I → c • x ≡ c • y [SMOD I • U]
-- Init.Data.Vector.Erase
Vector.eraseIdx_set : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {a : α} {hi : i < n} {j : ℕ} {hj : j < n},
  (xs.set i a hi).eraseIdx j hj =
    if h' : j < i then (xs.eraseIdx j hj).set (i - 1) a ⋯
    else if h'' : j = i then xs.eraseIdx i hi else (xs.eraseIdx j hj).set i a ⋯
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.Kernel.iIndepSet s κ μ →
      ∀ (S T : Set ι),
        Disjoint S T →
          ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {t | ∃ n ∈ S, s n = t})
            (MeasurableSpace.generateFrom {t | ∃ k ∈ T, s k = t}) κ μ
-- Mathlib.Data.Finset.Card
Finset.card_sdiff_eq_card_sdiff_iff : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], (s \ t).card = (t \ s).card ↔ s.card = t.card
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `toZMod` is a ring hom from `ℤ_[p]` to `ZMod p`,
with the equality `toZMod x = (zmodRepr x : ZMod p)`.
 -/
PadicInt.toZMod : {p : ℕ} → [hp_prime : Fact (Nat.Prime p)] → ℤ_[p] →+* ZMod p
-- Init.Meta.Defs
/-- Creates literal syntax for a number, which is provided as a string. The caller must ensure that the
string is a valid token for the `num` token parser.

If `info` is provided, then the literal's source information is copied from it.
 -/
Lean.Syntax.mkNumLit : String → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.NumLit
-- Mathlib.Topology.Algebra.Monoid
ContinuousOn.pow : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : Monoid M]
  [ContinuousMul M] {f : X → M} {s : Set X}, ContinuousOn f s → ∀ (n : ℕ), ContinuousOn (f ^ n) s
-- Mathlib.NumberTheory.MulChar.Basic
/-- **Alias** of `MulChar.domRestrict_apply`. -/
MulChar.restrict_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {S : Type u_3}
  [inst_2 : SetLike S R] [inst_3 : SubmonoidClass S R] (T : S) (χ : MulChar R R') (x : ↥T),
  (MulChar.domRestrict T χ) x = if IsUnit x then χ ↑x else 0
-- Mathlib.Algebra.Quaternion
Quaternion.inv_def : ∀ {R : Type u_1} [inst : Field R] (a : Quaternion R), a⁻¹ = (Quaternion.normSq a)⁻¹ • star a
-- Mathlib.Data.Nat.Init
/-- Decreasing induction: if `P (k+1)` implies `P k` for all `m ≤ k < n`, then `P n` implies `P m`.
Also works for functions to `Sort*`.

Weakens the assumptions of `Nat.decreasingInduction`.  -/
Nat.decreasingInduction' : {m n : ℕ} → {P : ℕ → Sort u_1} → ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → m ≤ n → P n → P m
-- Init.Data.String.Basic
/-- Given a string and two valid positions within the string, obtain a slice on the string formed by
the new bounds, or panic if the given end is strictly less than the given start.
 -/
String.slice! : (s : String) → s.Pos → s.Pos → String.Slice
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.smul_comp : ∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : AddZeroClass A] [inst_1 : AddZeroClass B]
  [inst_2 : AddZeroClass C] [inst_3 : DistribSMul M C] (m : M) (g : B →+ C) (f : A →+ B), (m • g).comp f = m • g.comp f
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.left_unitality : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) (F.obj X))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
        (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))
-- Mathlib.NumberTheory.Pell
/-- A solution has `x ≠ 0`.  -/
Pell.Solution₁.x_ne_zero : ∀ {d : ℤ}, 0 ≤ d → ∀ (a : Pell.Solution₁ d), a.x ≠ 0
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrTheoremCacheKey.mk.sizeOf_spec : ∀ (f : Lean.Expr) (numArgs : ℕ), sizeOf { f := f, numArgs := numArgs } = 1 + sizeOf f + sizeOf numArgs
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_strictMono_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, Function.Injective ⇑f → StrictMono (Submonoid.map f)
-- Std.Time.Date.Unit.Week
Std.Time.Week.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Week.Offset n