mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α},
  Std.DTreeMap.Const.get! (Std.DTreeMap.Const.unitOfList l cmp) k = ()
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo.mk.injEq : ∀ (us : List Lean.Level) (α β h : Lean.Expr) (inv? : Option (Lean.Expr × Lean.Expr)) (us_1 : List Lean.Level)
  (α_1 β_1 h_1 : Lean.Expr) (inv?_1 : Option (Lean.Expr × Lean.Expr)),
  ({ us := us, α := α, β := β, h := h, inv? := inv? } = { us := us_1, α := α_1, β := β_1, h := h_1, inv? := inv?_1 }) =
    (us = us_1 ∧ α = α_1 ∧ β = β_1 ∧ h = h_1 ∧ inv? = inv?_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.forInStep.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.forInStep f init (Std.DTreeMap.Internal.Impl.inner size k' v l r) = do
    let __do_lift ← Std.DTreeMap.Internal.Impl.forInStep f init l
    match __do_lift with
      | ForInStep.done d => pure (ForInStep.done d)
      | ForInStep.yield d => do
        let __do_lift ← f k' v d
        match __do_lift with
          | ForInStep.done d => pure (ForInStep.done d)
          | ForInStep.yield d => Std.DTreeMap.Internal.Impl.forInStep f d r
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_erase_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).size ≤ t.size
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.abs_expect_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] [PosSMulMono ℚ≥0 α] (s : Finset ι) (f : ι → α),
  |s.expect fun i => f i| ≤ s.expect fun i => |f i|
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.comp_comparison_forget_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D)
  (R : CategoryTheory.Functor D C) [inst_3 : CategoryTheory.MonadicRightAdjoint R]
  [CategoryTheory.Limits.HasLimit (F.comp R)],
  CategoryTheory.Limits.HasLimit
    ((F.comp (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R))).comp
      (CategoryTheory.monadicAdjunction R).toMonad.forget)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.Context : Type
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run a custom tactic at every step in proofs, configured via environment variables.

Set `TRY_AT_EACH_STEP_TACTIC` to the tactic syntax to try (required).
Set `TRY_AT_EACH_STEP_LABEL` to the label for output messages (optional, defaults to tactic).
 -/
tryAtEachStepFromEnv : Mathlib.TacticAnalysis.Config
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.hasSubst_def : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] (a : σ → MvPowerSeries τ S),
  MvPowerSeries.HasSubst a ↔
    (∀ (s : σ), IsNilpotent (MvPowerSeries.constantCoeff (a s))) ∧
      ∀ (d : τ →₀ ℕ), {s | (MvPowerSeries.coeff d) (a s) ≠ 0}.Finite
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_subset : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M},
  s ⊆ t → UniqueMDiffAt[s] x → MDiffAt[t] f x → mfderiv[s] f x = mfderiv[t] f x
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigits_SurjOn : ∀ {b : ℕ}, 1 < b → Set.SurjOn Real.ofDigits Set.univ (Set.Icc 0 1)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.smul_eq_comp_mk₀ : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C] {X Y : C}
  {n : ℕ} (x : CategoryTheory.Abelian.Ext X Y n) (r : R),
  r • x = x.comp (CategoryTheory.Abelian.Ext.mk₀ (r • CategoryTheory.CategoryStruct.id Y)) ⋯
-- Mathlib.CategoryTheory.Endomorphism
/-- Multiplication of endomorphisms agrees with `Function.comp`, not with
`CategoryTheory.CategoryStruct.comp`.  -/
CategoryTheory.End.mul : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → (X : C) → Mul (CategoryTheory.End X)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- If a preadditive category has all weak kernels, then it also has all weak equalizers.  -/
CategoryTheory.Preadditive.hasWeakEqualizers_of_hasWeakKernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasWeakKernels C], CategoryTheory.Limits.HasWeakEqualizers C
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_modify_eq_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α], t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).minKey! = t.minKey!
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DTreeMap.Raw.Const.get? (m₁ ∩ m₂) k = none
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  0 < t →
    ∫ (x : Ω), X x ∂μ = 0 →
      Set.Icc 0 t ⊆ interior (ProbabilityTheory.integrableExpSet X μ) →
        ∃ u ∈ Set.Ioo 0 t, ProbabilityTheory.cgf X μ t = iteratedDeriv 2 (ProbabilityTheory.cgf X μ) u * t ^ 2 / 2
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- The value of the Infimum of a nonempty family of outer measures on a set is not simply
the minimum value of a measure on that set: it is the infimum sum of measures of countable set of
sets that covers that set, where a different measure can be used for each set in the cover.  -/
MeasureTheory.OuterMeasure.biInf_apply : ∀ {α : Type u_1} {ι : Type u_2} {I : Set ι},
  I.Nonempty →
    ∀ (m : ι → MeasureTheory.OuterMeasure α) (s : Set α),
      (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
-- Init.Data.BitVec.Lemmas
BitVec.lt_def : ∀ {n : ℕ} {x y : BitVec n}, x < y ↔ x.toNat < y.toNat
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_sup : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (S T : Submodule R M), -(S ⊔ T) = -S ⊔ -T
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_add : ∀ (x y : ℂ), Complex.cos (x + y) = Complex.cos x * Complex.cos y - Complex.sin x * Complex.sin y
-- Mathlib.RingTheory.Congruence.Basic
/-- The map sending a binary relation to the smallest congruence relation in which it is
contained is idempotent.  -/
RingCon.ringConGen_idem : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (r : R → R → Prop), ringConGen ⇑(ringConGen r) = ringConGen r
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_lt_iff_lt_one_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosStrictMono α]
  [MulPosReflectLT α], 0 < b → (a * b < b ↔ a < 1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.tail_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, SimpleGraph.Walk.nil.tail = SimpleGraph.Walk.nil
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n`-th iterated derivative of a function from `𝕜` to `F` within a set `s`, as a function
from `𝕜` to `F`.  -/
iteratedDerivWithin : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} → [inst_1 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → ℕ → (𝕜 → F) → Set 𝕜 → 𝕜 → F
-- Init.Data.List.Sort.Lemmas
List.mergeSort_perm : ∀ {α : Type u_1} (l : List α) (le : α → α → Bool), (l.mergeSort le).Perm l
-- Mathlib.Algebra.DualNumber
/-- Lifting `DualNumber.eps` itself gives the identity.  -/
DualNumber.lift_inlAlgHom_eps : ∀ {R : Type u_1} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  DualNumber.lift ⟨(TrivSqZeroExt.inlAlgHom R A A, DualNumber.eps), ⋯⟩ = AlgHom.id R (DualNumber A)
-- Init.Data.Array.Range
Array.zipIdx_map : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {k : ℕ} {f : α → β},
  (Array.map f xs).zipIdx k = Array.map (Prod.map f id) (xs.zipIdx k)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanDeclIdent.fromJson : Lean.Json → Except String Lean.Lsp.LeanDeclIdent
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- If `A` and `B` are modules, homeomorphic via a semilinear homeomorphism, and if
`A` has the module topology, then so does `B`.  -/
IsModuleTopology.isoₛₗ : ∀ {R : Type u_1} {S : Type u_2} [τR : TopologicalSpace R] [τS : TopologicalSpace S] [inst : Semiring R]
  [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
  {A : Type u_3} [inst_4 : AddCommMonoid A] [inst_5 : Module R A] [τA : TopologicalSpace A] [IsModuleTopology R A]
  {B' : Type u_5} [inst_7 : AddCommMonoid B'] [inst_8 : Module S B'] [τB' : TopologicalSpace B'],
  Continuous ⇑σ → Continuous ⇑σ' → ∀ (e : A ≃SL[σ] B'), IsModuleTopology S B'
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_ne_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → ∀ (i : Fin (n + 1)), s.excenter signs ≠ s.points i
-- Mathlib.RingTheory.FiniteType
/-- If an additive monoid `M` is finitely generated then `R[M]` is of finite
type.  -/
AddMonoidAlgebra.finiteType_of_fg : ∀ (R : Type u_1) (M : Type u_2) [inst : AddMonoid M] [inst_1 : CommRing R] [h : AddMonoid.FG M],
  Algebra.FiniteType R (AddMonoidAlgebra R M)
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.coproductCocone_inl : ∀ (A B : CommRingCat), (A.coproductCocone B).inl = CommRingCat.ofHom Algebra.TensorProduct.includeLeft.toRingHom
-- Mathlib.FieldTheory.SeparableClosure
/-- The separable closure of `F` in `E` is equal to `E` if and only if `E / F` is
separable.  -/
separableClosure.eq_top_iff : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  separableClosure F E = ⊤ ↔ Algebra.IsSeparable F E
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstHDivNat : Lean.Expr → Lean.MetaM Bool
-- Batteries.Data.Char.Basic
Char.toNat_le_max : ∀ (c : Char), c.toNat ≤ Char.max
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_lt_iff_lt_exp : ∀ {x y : ℝ}, 0 < x → (Real.log x < y ↔ x < Real.exp y)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_eval_eq_apply : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : CommSemiring R] (M : Matrix m n R) (i : m)
  (c : n → R), (MvPolynomial.eval c) (M.toMvPolynomial i) = M.mulVec c i
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd : ∀ {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [NeZero m]
  [hK : IsCyclotomicExtension {m} ℚ K],
  ¬p ∣ m → (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = orderOf ↑p
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_image_iterateFrobenius : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p n : ℕ} [inst_2 : ExpChar R p] {f : Polynomial R}
  [PerfectRing R p] [inst_4 : DecidableEq R],
  Finset.image (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuousAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  LowerHemicontinuousAt f x ↔ ∀ (u : Set β), IsOpen u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in nhds x, (f x' ∩ u).Nonempty
-- Init.Omega.Constraint
Lean.Omega.normalize?_eq_some : ∀ {s : Lean.Omega.Constraint} {x : Lean.Omega.Coeffs} {s' : Lean.Omega.Constraint} {x' : Lean.Omega.Coeffs},
  Lean.Omega.normalize? (s, x) = some (s', x') →
    Lean.Omega.normalizeConstraint s x = s' ∧ Lean.Omega.normalizeCoeffs s x = x'
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.lt_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LT ι] [inst_2 : (i : ι) → LT (α i)]
  {a b : Lex (Π₀ (i : ι), α i)}, a < b ↔ ∃ i, (∀ j < i, (ofLex a) j = (ofLex b) j) ∧ (ofLex a) i < (ofLex b) i
-- Mathlib.Order.Partition.Basic
/-- The function maps each element in the support to a related element.  -/
Partition.IsRepFun.rel_apply : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α}, P.IsRepFun f → ∀ ⦃a : α⦄, a ∈ u → P.Rel a (f a)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.mem_skeletonLT_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {x : X},
  x ∈ Topology.RelCWComplex.skeletonLT C n ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
-- Lean.Message
Lean.MessageData.group.injEq : ∀ (a a_1 : Lean.MessageData), (a.group = a_1.group) = (a = a_1)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The universal morphism `universalAddHom` is unique.  -/
AddOreLocalization.universalAddHom_unique : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {T : Type u_2}
  [inst_2 : AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s))
  (φ : AddOreLocalization S R →+ T),
  (∀ (r : R), φ (AddOreLocalization.numeratorHom r) = f r) → φ = AddOreLocalization.universalAddHom f fS hf
-- Init.Data.Int.Lemmas
Int.eq_of_mul_eq_mul_left : ∀ {a b c : ℤ}, a ≠ 0 → a * b = a * c → b = c
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.addCommMagma.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : AddCommMagma M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Surjective.addCommMagma f hf mul = { toAdd := inst, add_comm := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instIsVeryGoodOfFactorizationData : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.diag A)),
  (HomotopicalAlgebra.PathObject.ofFactorizationData h).IsVeryGood
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleAlgebra.toIsScalarTower : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieAdmissibleRing L} [self : LieAdmissibleAlgebra R L],
  IsScalarTower R L L
-- Mathlib.Order.CountableSupClosed
isGLB_countableInfClosure : ∀ {α : Type u_2} {s : Set α} {a : α} [inst : Preorder α], IsGLB (countableInfClosure s) a ↔ IsGLB s a
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMaps.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasImages C],
  CategoryTheory.Limits.HasImageMaps C = CategoryTheory.Limits.HasImageMaps C
-- Mathlib.Algebra.Order.Module.Defs
PosSMulStrictMono.toPosSMulReflectLE : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β] [inst_3 : Zero α]
  [PosSMulStrictMono α β], PosSMulReflectLE α β
-- Init.Data.List.Find
List.find?_filterMap : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β} {p : β → Bool},
  List.find? p (List.filterMap f xs) = (List.find? (fun a => Option.any p (f a)) xs).bind f
-- Mathlib.Order.Atoms
SuccOrder.toIsStronglyAtomic : ∀ {α : Type u_4} [inst : Preorder α] [SuccOrder α], IsStronglyAtomic α
-- Mathlib.RingTheory.Extension.Presentation.Submersive
_private.Mathlib.RingTheory.Extension.Presentation.Submersive.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_₁₂ : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_7 : Fintype σ] [inst_8 : Fintype σ'],
  (Q.comp P).jacobiMatrix.toBlocks₁₂ = 0
-- Lean.Elab.Command.Scope
Lean.Elab.Command.Scope.mk : String →
  Lean.Options →
    Lean.Name →
      List Lean.OpenDecl →
        List Lean.Name →
          Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder) →
            Array Lean.Name →
              List Lean.Name →
                List Lean.Name →
                  Bool → Bool → Bool → List (Lean.TSyntax `Lean.Parser.Term.attrInstance) → Lean.Elab.Command.Scope
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_top : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L), x ∈ ⊤
-- Init.Data.Array.Lex.Lemmas
Array.le_total : ∀ {α : Type u_1} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] (xs ys : Array α), xs ≤ ys ∨ ys ≤ xs
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.finset_prod : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : CommMonoid β] {ι : Type u_9} {s : Finset ι}
  {f : ι → α → β}, (∀ i ∈ s, HasCompactMulSupport (f i)) → HasCompactMulSupport (∏ i ∈ s, f i)
-- Mathlib.Tactic.Linarith.Frontend
/-- `linarithUsedHyps only_on hyps cfg g` runs `linarith` with the supplied hypotheses. It
fails if the goal cannot be closed. When successful, it returns the subset of `hyps` that
were actually used (i.e. had a nonzero coefficient) in the final certificate.

* `hyps` is a list of proofs of comparisons to include in the search.
* If `only_on` is true, the search will be restricted to `hyps`. Otherwise it will use all
  comparisons in the local context.
* If `cfg.transparency := semireducible`,
  it will unfold semireducible definitions when trying to match atomic expressions.
 -/
Mathlib.Tactic.Linarith.linarithUsedHyps : Bool → List Lean.Expr → optParam Mathlib.Tactic.Linarith.LinarithConfig { } → Lean.MVarId → Lean.MetaM (List Lean.Expr)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.keys_perm : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β}, m₁.Equiv m₂ → m₁.keys.Perm m₂.keys
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `x` and `y` are distinct letters and `w₁ w₂` are words such that `x + w₁`
reduces to `y + w₂`, then `w₁` reduces to `-x + y + w₂`.  -/
FreeAddGroup.Red.neg_of_red_of_ne : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool},
  (x1, b1) ≠ (x2, b2) →
    FreeAddGroup.Red ((x1, b1) :: L₁) ((x2, b2) :: L₂) → FreeAddGroup.Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
-- Init.Data.ByteArray.Basic
/-- The reference implementation of `ForIn.forIn` for `ByteArray`.

In compiled code, this is replaced by the more efficient `ByteArray.forInUnsafe`.
 -/
ByteArray.forIn : {β : Type v} → {m : Type v → Type w} → [Monad m] → ByteArray → β → (UInt8 → β → m (ForInStep β)) → m β
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
EuclideanSpace.volume_closedBall : ∀ (ι : Type u_1) [Nonempty ι] [inst : Fintype ι] (x : EuclideanSpace ℝ ι) (r : ℝ),
  MeasureTheory.volume (Metric.closedBall x r) =
    ENNReal.ofReal r ^ Fintype.card ι *
      ENNReal.ofReal (√Real.pi ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / 2 + 1))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw.buckets_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c i : ℕ} {h : i < (Std.DHashMap.Raw.emptyWithCapacity c).buckets.size},
  (Std.DHashMap.Raw.emptyWithCapacity c).buckets[i] = Std.DHashMap.Internal.AssocList.nil
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instCommRing : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] → [inst_3 : CommSemiring B] → [inst_4 : Algebra R B] → CommRing (TensorProduct R A B)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ofUnitHom_coe : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ),
  (MulChar.ofUnitHom f) ↑a = ↑(f a)
-- Mathlib.GroupTheory.CommutingProbability
Subgroup.commProb_subgroup_le : ∀ {G : Type u_2} [inst : Group G] [Finite G] (H : Subgroup G), commProb ↥H ≤ commProb G * ↑H.index ^ 2
-- Aesop.Tree.Data
Aesop.Rapp.metaState : Aesop.Rapp → Lean.Meta.SavedState
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.instIsCofilteredStructuredArrowCompOfRepresentablyFlat : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : E) [CategoryTheory.RepresentablyFlat F]
  [CategoryTheory.IsCofiltered (CategoryTheory.StructuredArrow X G)],
  CategoryTheory.IsCofiltered (CategoryTheory.StructuredArrow X (F.comp G))
-- Init.Data.UInt.Lemmas
USize.neg_sub : ∀ {a b : USize}, -(a - b) = b - a
-- Lean.Parser.Extra
Lean.Parser.sepBy1.formatter : Lean.PrettyPrinter.Formatter →
  String → Lean.PrettyPrinter.Formatter → optParam Bool false → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_im_ne_zero : ∀ {g : GL (Fin 2) ℝ} {z : ℂ}, ((UpperHalfPlane.σ g) z).im ≠ 0 ↔ z.im ≠ 0
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.adjoin_iff_disjoint : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x →
    ∀ [Nontrivial A] {s t : Set ι}, (AlgebraicIndependent ↥(Algebra.adjoin R (x '' s)) fun i => x ↑i) ↔ Disjoint s t
-- Mathlib.Analysis.SpecialFunctions.CompareExp
/-- If `l : Filter ℂ` is an "exponential comparison filter", then $\log |z| =o(ℜ z)$ along `l`.
This is the main lemma in the proof of `Complex.IsExpCmpFilter.isLittleO_cpow_exp` below.
 -/
Complex.IsExpCmpFilter.isLittleO_log_norm_re : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → (fun z => Real.log ‖z‖) =o[l] Complex.re
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
/-- A (semi-)linear map which is a homothety is a continuous linear map.
Since the field `𝕜` need not have `ℝ` as a subfield, this theorem is not directly deducible from
the corresponding theorem about isometries plus a theorem about scalar multiplication.  Likewise
for the other theorems about homotheties in this file.
 -/
ContinuousLinearMap.ofHomothety : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [inst : Ring 𝕜] →
          [inst_1 : Ring 𝕜₂] →
            [inst_2 : SeminormedAddCommGroup E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜₂ F] →
                    {σ : 𝕜 →+* 𝕜₂} → (f : E →ₛₗ[σ] F) → (a : ℝ) → (∀ (x : E), ‖f x‖ = a * ‖x‖) → E →SL[σ] F
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Asymptotics.IsEquivalent.summable_iff : ∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  {f g : ι → E}, Asymptotics.IsEquivalent Filter.cofinite f g → (Summable f ↔ Summable g)