mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Constructible
/-- [Stacks Tag 09YE](https://stacks.math.columbia.edu/tag/09YE) -/
Topology.IsConstructible.preimage_of_isClosedEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Topology.IsClosedEmbedding f →
    IsCompact (Set.range f)ᶜ → Topology.IsConstructible s → Topology.IsConstructible (f ⁻¹' s)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- A variant of `RightHomotopy.compLeft` useful for dealing with homotopy equivalences.  -/
CategoryTheory.Arrow.RightHomotopy.compLeftId : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f : v ⟶ v} →
          CategoryTheory.Arrow.RightHomotopy f (CategoryTheory.CategoryStruct.id v) →
            (g : u ⟶ v) → CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp g f) g
-- Mathlib.GroupTheory.Solvable
/-- The derived series of the group `G`, obtained by starting from the subgroup `⊤` and repeatedly
taking the commutator of the previous subgroup with itself for `n` times.  -/
derivedSeries : (G : Type u_1) → [inst : Group G] → ℕ → Subgroup G
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clauses_performRupCheck : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array ℕ),
  (f.performRupCheck rupHints).1.clauses = f.clauses
-- Mathlib.RingTheory.Congruence.Defs
RingCon.ext_iff : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, c = d ↔ ∀ (x y : R), c x y ↔ d x y
-- Mathlib.Data.Set.Operations
Set.mem_univ_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {f : (i : ι) → α i},
  f ∈ Set.univ.pi t ↔ ∀ (i : ι), f i ∈ t i
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.eq_1 : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] (f : ℝ → X) (a b : ℝ),
  AbsolutelyContinuousOnInterval f a b =
    Filter.Tendsto (fun E => ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2))
      (AbsolutelyContinuousOnInterval.totalLengthFilter ⊓
        Filter.principal (AbsolutelyContinuousOnInterval.disjWithin a b))
      (nhds 0)
-- Mathlib.Order.CompleteLattice.Basic
biSup_sup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α},
  (∃ i, p i) → (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a
-- Lean.Elab.Tactic.Split
_private.Lean.Elab.Tactic.Split.0.Lean.Elab.Tactic.evalSplit.throwCouldNotSplitGoal : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.RingTheory.SimpleModule.Basic
isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective : ∀ {S : Type u_3} [inst : Ring S] {M : Type u_4} [inst_1 : AddCommGroup M] {R : Type u_6} [inst_2 : CommRing R]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M],
  Function.Surjective ⇑(algebraMap R S) → (IsSimpleModule R M ↔ IsSimpleModule S M)
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Paths.of_obj : ∀ (V : Type u₁) [inst : Quiver V] (X : V), (CategoryTheory.Paths.of V).obj X = X
-- Mathlib.RingTheory.Congruence.Hom
/-- An isomorphism of rings `e : M ≃+* N` generates an isomorphism between quotient spaces,
if it is compatible with the relations.  -/
RingCon.congr : {M : Type u_1} →
  {N : Type u_2} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring N] →
        {c : RingCon M} → {d : RingCon N} → (e : M ≃+* N) → c = d.comap e → c.Quotient ≃+* d.Quotient
-- Init.Data.Vector.Lemmas
/-- Use this as `induction ass using vector₂_induction` on a hypothesis of the form `ass : Vector (Vector α n) m`.
The hypothesis `ass` will be replaced with a hypothesis `ass : Array (Array α)`
along with additional hypotheses `h₁ : ass.size = m` and `h₂ : ∀ xs ∈ ass, xs.size = n`.
Appearances of the original `ass` in the goal will be replaced with
`Vector.mk (xss.attach.map (fun ⟨xs, m⟩ => Vector.mk xs ⋯)) ⋯`.
 -/
Vector.vector₂_induction : ∀ {α : Type u_1} {n m : ℕ} (P : Vector (Vector α n) m → Prop),
  (∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ xs ∈ xss, xs.size = n),
      P
        (Vector.mk
          (Array.map
            (fun x =>
              match x with
              | ⟨xs, m⟩ => Vector.mk xs ⋯)
            xss.attach)
          ⋯)) →
    ∀ (xss : Vector (Vector α n) m), P xss
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_map_const_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsProbabilityMeasure μ]
  (c : E),
  ProbabilityTheory.covarianceBilin (MeasureTheory.Measure.map (fun x => c + x) μ) = ProbabilityTheory.covarianceBilin μ
-- Init.Data.BitVec.Lemmas
BitVec.toInt_one_of_lt : ∀ {w : ℕ}, 1 < w → (1#w).toInt = 1
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Lebesgue dominated convergence theorem for series.  -/
MeasureTheory.hasSum_integral_of_dominated_convergence : ∀ {α : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_4} [Countable ι] {F : ι → α → G} {f : α → G} (bound : ι → α → ℝ),
  (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) μ) →
    (∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a) →
      (∀ᵐ (a : α) ∂μ, Summable fun n => bound n a) →
        MeasureTheory.Integrable (fun a => ∑' (n : ι), bound n a) μ →
          (∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)) → HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
-- Mathlib.Algebra.Polynomial.Inductions
/-- A property holds for all polynomials of positive `degree` with coefficients in a semiring `R`
if it holds for
* `a * X`, with `a ∈ R`,
* `p * X`, with `p ∈ R[X]`,
* `p + a`, with `a ∈ R`, `p ∈ R[X]`,

with appropriate restrictions on each term.

See `natDegree_ne_zero_induction_on` for a similar statement involving no explicit multiplication.
 -/
Polynomial.degree_pos_induction_on : ∀ {R : Type u} [inst : Semiring R] {P : Polynomial R → Prop} (p : Polynomial R),
  0 < p.degree →
    (∀ {a : R}, a ≠ 0 → P (Polynomial.C a * Polynomial.X)) →
      (∀ {p : Polynomial R}, 0 < p.degree → P p → P (p * Polynomial.X)) →
        (∀ {p : Polynomial R} {a : R}, 0 < p.degree → P p → P (p + Polynomial.C a)) → P p
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- We may want to endow an affine space with a `MeasureSpace` that transfers `volume` from its
associated inner product space. If it is implemented, we can unify this lemma with the previous one.
 -/
EuclideanGeometry.euclideanHausdorffMeasure_eq : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (p : P),
  MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V) =
    MeasureTheory.Measure.map (⇑(IsometryEquiv.vaddConst p)) MeasureTheory.volume
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_sUnion : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (s : Set α) (T : Set (Set β)), s +ᵥ ⋃₀ T = ⋃ t ∈ T, s +ᵥ t
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_of_eq_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly → Bool
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by changing the lower bound if another value `j` satisfies the same
constraint.
 -/
Std.Time.Internal.Bounded.LE.truncateBottom : {n m j : ℤ} → (bounded : Std.Time.Internal.Bounded.LE n m) → ↑bounded ≥ j → Std.Time.Internal.Bounded.LE j m
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
CategoryTheory.Limits.instHasFiniteColimitsFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Functor K C)
-- Mathlib.GroupTheory.Torsion
/-- A predicate on a monoid saying that all elements are of finite order.  -/
IsMulTorsion : (G : Type u_1) → [Monoid G] → Prop
-- Mathlib.Probability.Kernel.Composition.Comp
/-- Composition of two kernels.  -/
ProbabilityTheory.«term_∘ₖ_» : Lean.TrailingParserDescr
-- Mathlib.Order.Ideal
/-- **Alias** of the reverse direction of `Order.Ideal.iSup_mem_iff`. -/
Order.Ideal.iSup_mem : ∀ {P : Type u_1} [inst : CompleteLattice P] {I : Order.Ideal P} {α : Sort u_2} [Finite α] {f : α → P},
  (∀ (i : α), f i ∈ I) → ⨆ i, f i ∈ I
-- Mathlib.Control.Fold
Traversable.toList_eq_self : ∀ {α : Type u} {xs : List α}, Traversable.toList xs = xs
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.add_neg_cancel : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] (a : M), a + -a = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The canonical isomorphism `(mappingCone (homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X q`
when `p + 1 = q`.  -/
CochainComplex.mappingConeHomOfDegreewiseSplitXIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) →
        (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) →
          [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
            (p q : ℤ) →
              p + 1 = q → ((CochainComplex.mappingCone (CochainComplex.homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X q)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.iteratedFDerivLM_apply_of_le : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ}
  (f : ContDiffMapSupportedIn E F n K),
  k + ↑i ≤ n → ⇑((ContDiffMapSupportedIn.iteratedFDerivLM 𝕜 n k i) f) = iteratedFDeriv ℝ i ⇑f
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
ContinuousLinearEquiv.arrowCongrSL.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  {H : Type u_8} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ σ₁₃_1 : 𝕜 →+* 𝕜₃} (e_σ₁₃ : σ₁₃ = σ₁₃_1) {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃}
  {σ₂₄ σ₂₄_1 : 𝕜₂ →+* 𝕜₄} (e_σ₂₄ : σ₂₄ = σ₂₄_1) {σ₁₄ : 𝕜 →+* 𝕜₄} [inst_20 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃] [inst_23 : RingHomInvPair σ₄₃ σ₃₄]
  [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [inst_30 : RingHomIsometric σ₁₂]
  [inst_31 : RingHomIsometric σ₂₁] (e₁₂ e₁₂_1 : ⋯), ⋯
-- Mathlib.Data.Nat.Count
Nat.count_le_card : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (hp : (Set.ofPred p).Finite) (n : ℕ), Nat.count p n ≤ hp.toFinset.card
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- The structure presheaf, valued in `CommRing`, constructed by dressing up the `Type`-valued
structure presheaf.  -/
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → TopCat.Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  t.isEmpty = true → t.getKeyD a fallback = fallback
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.rightHom.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  SemidirectProduct.rightHom = { toFun := SemidirectProduct.right, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.GroupTheory.GroupAction.Pointwise
AddMonoidHom.preimage_vadd_setₛₗ : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N]
  [inst_2 : AddAction M α] [inst_3 : AddAction N β] {c : M} {F : Type u_6} (σ : M →+ N) [inst_4 : FunLike F α β]
  [AddActionSemiHomClass F (⇑σ) α β] (f : F), IsAddUnit c → ∀ (t : Set β), ⇑f ⁻¹' (σ c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- A finite type torsion free module over a PID admits a basis.  -/
Module.basisOfFiniteTypeTorsionFree : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsPrincipalIdealRing R] →
              [IsDomain R] →
                [Fintype ι] →
                  {s : ι → M} →
                    Submodule.span R (Set.range s) = ⊤ → [Module.IsTorsionFree R M] → (n : ℕ) × Module.Basis (Fin n) R M
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.funUnique_apply : ∀ (α : Type u_2) (M : Type u_4) [inst : Mul M] [inst_1 : Unique α] (f : (i : α) → (fun a => M) i),
  (MulEquiv.funUnique α M) f = f default
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.mk.inj : ∀ {id : ℕ} {type : Lean.Expr} {u : Lean.Level} {op : Lean.Expr} {neutral? : Option Lean.Expr} {assocInst : Lean.Expr}
  {idempotentInst? commInst? neutralInst? : Option Lean.Expr} {nextId : ℕ} {vars : Lean.PArray Lean.Expr}
  {varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Var}
  {denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Expr}
  {denoteEntries : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)} {queue : Lean.Meta.Grind.AC.Queue}
  {basis : List Lean.Meta.Grind.AC.EqCnstr} {diseqs : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr} {recheck : Bool}
  {id_1 : ℕ} {type_1 : Lean.Expr} {u_1 : Lean.Level} {op_1 : Lean.Expr} {neutral?_1 : Option Lean.Expr}
  {assocInst_1 : Lean.Expr} {idempotentInst?_1 commInst?_1 neutralInst?_1 : Option Lean.Expr} {nextId_1 : ℕ}
  {vars_1 : Lean.PArray Lean.Expr} {varMap_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Var}
  {denote_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.AC.Expr}
  {denoteEntries_1 : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)} {queue_1 : Lean.Meta.Grind.AC.Queue}
  {basis_1 : List Lean.Meta.Grind.AC.EqCnstr} {diseqs_1 : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr} {recheck_1 : Bool},
  { id := id, type := type, u := u, op := op, neutral? := neutral?, assocInst := assocInst,
        idempotentInst? := idempotentInst?, commInst? := commInst?, neutralInst? := neutralInst?, nextId := nextId,
        vars := vars, varMap := varMap, denote := denote, denoteEntries := denoteEntries, queue := queue,
        basis := basis, diseqs := diseqs, recheck := recheck } =
      { id := id_1, type := type_1, u := u_1, op := op_1, neutral? := neutral?_1, assocInst := assocInst_1,
        idempotentInst? := idempotentInst?_1, commInst? := commInst?_1, neutralInst? := neutralInst?_1,
        nextId := nextId_1, vars := vars_1, varMap := varMap_1, denote := denote_1, denoteEntries := denoteEntries_1,
        queue := queue_1, basis := basis_1, diseqs := diseqs_1, recheck := recheck_1 } →
    id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          op = op_1 ∧
            neutral? = neutral?_1 ∧
              assocInst = assocInst_1 ∧
                idempotentInst? = idempotentInst?_1 ∧
                  commInst? = commInst?_1 ∧
                    neutralInst? = neutralInst?_1 ∧
                      nextId = nextId_1 ∧
                        vars = vars_1 ∧
                          varMap = varMap_1 ∧
                            denote = denote_1 ∧
                              denoteEntries = denoteEntries_1 ∧
                                queue = queue_1 ∧ basis = basis_1 ∧ diseqs = diseqs_1 ∧ recheck = recheck_1
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_linearMap_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  Function.Injective fun x => ↑x
-- Init.Data.List.Nat.Range
List.take_range : ∀ {i n : ℕ}, List.take i (List.range n) = List.range (min i n)
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.add_mul_mul_mul_invOf_eq_one : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
  [inst_5 : Invertible A] [inst_6 : Invertible (C + C * V * ⅟A * U * C)],
  (A + U * C * V) * (⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) = 1
-- Init.Prelude
/-- Anything follows from two contradictory hypotheses. Example:
```
example (hp : p) (hnp : ¬p) : q := absurd hp hnp
```
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
 -/
absurd : {a : Prop} → {b : Sort v} → a → ¬a → b
-- Mathlib.Algebra.Lie.Subalgebra
LieHom.mem_range_self : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (x : L), f x ∈ f.range
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.toNormalizedChainComplex_f_fromNormalizedChainComplex_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) {Z : C} (h : (X.chainComplex R).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((X.toNormalizedChainComplex R).f n)
      (CategoryTheory.CategoryStruct.comp ((X.fromNormalizedChainComplex R).f n) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey?_alterKey_eq_self : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.maxKey? (Std.Internal.List.Const.alterKey k f l) = some k ↔
      (f (Std.Internal.List.getValue? k l)).isSome = true ∧
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.instFaithfulSimplexCategory : CategoryTheory.Functor.Faithful SSet.stdSimplex
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α}, (Std.ExtTreeMap.filterMap f t)[k]? = t[k]?.pbind fun x h' => f (t.getKey k ⋯) x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `C` has all limits of diagrams `pair X Y`, then it has all binary products  -/
CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [∀ {X Y : C}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)],
  CategoryTheory.Limits.HasBinaryProducts C
-- Std.Time.DateTime.WallTime
/-- Adds a `Week.Offset` to the given `WallTime`.
 -/
Std.Time.WallTime.addWeeks : Std.Time.WallTime → Std.Time.Week.Offset → Std.Time.WallTime
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of the reverse direction of `Set.disjoint_compl_left_iff_subset`. -/
HasSubset.Subset.disjoint_compl_left : ∀ {α : Type u_1} {s t : Set α}, t ⊆ s → Disjoint sᶜ t
-- Mathlib.Tactic.Translate.Core
/-- The global `do_translate`/`dont_translate` attributes specify whether operations on
a given type should be translated. `dont_translate` can be used for types that are translated,
such as `MonoidAlgebra` -> `AddMonoidAlgebra`, or for fixed types, such as `Fin n`/`ZMod n`.
`do_translate` is for types without arguments, like `Unit` and `Empty`, where the structure on it
can be translated.

Note: The name generation is not aware of `dont_translate`, so if some part of a lemma is not
  translated thanks to this, you generally have to specify the translated name manually.
 -/
Mathlib.Tactic.Translate.TranslateData.doTranslateAttr : Mathlib.Tactic.Translate.TranslateData → Lean.NameMapExtension Bool
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommMon C),
  (CategoryTheory.Functor.mapCommMonIdIso.inv.app X).hom.hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
/-- `Nat.doubleFactorial n` is the double factorial of `n`.  -/
Nat.doubleFactorial : ℕ → ℕ
-- Mathlib.Dynamics.Minimal
IsOpen.iUnion_preimage_smul : ∀ (M : Type u_1) {α : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [MulAction.IsMinimal M α] {U : Set α}, IsOpen U → U.Nonempty → ⋃ c, (fun x => c • x) ⁻¹' U = Set.univ
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiAlgebra : ∀ {𝕜 : Type u} {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {A : Type u_1}
  [inst_2 : NormedCommRing A] [inst_3 : NormedAlgebra 𝕜 A] [NormOneClass A],
  ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_pow' : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ},
  p.leadingCoeff ^ n ≠ 0 → (p ^ n).natDegree = n * p.natDegree
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- A simplified version of the previous theorem, for use in proofs by induction and the like.  -/
trapezoidal_integral_ext : ∀ {f : ℝ → ℝ} {N : ℕ} {a h : ℝ},
  0 < N →
    trapezoidal_integral f N a (a + ↑N * h) + trapezoidal_integral f 1 (a + ↑N * h) (a + (↑N + 1) * h) =
      trapezoidal_integral f (N + 1) a (a + (↑N + 1) * h)
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.measure.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (keys : Subarray α) (vals : Subarray β)
  (hsz : Std.Slice.size keys = Std.Slice.size vals) (z' : Lean.PersistentHashMap.Zipper α β),
  (Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z').measure = Std.Slice.size vals + z'.measure + 1
-- Batteries.Data.List.Matcher
List.Matcher.mk : {α : Type u_1} → Array.Matcher α → List α → List.Matcher α
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.map_cobounded : ∀ {X : Type u_1} {Y : Type u_2} {F : Type u_3} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y]
  [inst_2 : EquivLike F X Y] [DilationEquivClass F X Y] (e : F),
  Filter.map (⇑e) (Bornology.cobounded X) = Bornology.cobounded Y
-- Mathlib.GroupTheory.CoprodI
/-- A non-empty reduced word determines an element of the free product, given by multiplication.  -/
Monoid.CoprodI.NeWord.prod : {ι : Type u_1} →
  {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i j : ι} → Monoid.CoprodI.NeWord M i j → Monoid.CoprodI M