mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_comp_of_range_eq_top : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {τ₁₂ : R →+* R₂}
  {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] [inst_10 : RingHomSurjective τ₁₂]
  [inst_11 : RingHomSurjective τ₂₃] [inst_12 : RingHomSurjective τ₁₃] {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃),
  f.range = ⊤ → (g ∘ₛₗ f).range = g.range
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lsum_comp_lsingle : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R₂ N] {σ : R →+* R₂} [inst_7 : Module S N] [inst_8 : SMulCommClass R₂ S N]
  (f : α → M →ₛₗ[σ] N) (i : α), (Finsupp.lsum S) f ∘ₛₗ Finsupp.lsingle i = f i
-- Mathlib.Data.Vector.Basic
List.Vector.get_eq_get_toList : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : Fin n), v.get i = v.toList.get (Fin.cast ⋯ i)
-- Mathlib.FieldTheory.Fixed
IsInvariantSubfield.toMulSemiringAction : (M : Type u) →
  [inst : Monoid M] →
    {F : Type v} →
      [inst_1 : Field F] →
        [inst_2 : MulSemiringAction M F] → (S : Subfield F) → [IsInvariantSubfield M S] → MulSemiringAction M ↥S
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.union : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C],
  ⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n j = C
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- `y` is a conjugate root of `x` over `K` if and only if `y` is a root of the minimal polynomial of
`x`. This is variant of `isConjRoot_iff_aeval_eq_zero`.
 -/
isConjRoot_iff_mem_minpoly_aroots : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [inst_3 : IsDomain S]
  {x y : S}, IsIntegral K x → (IsConjRoot K x y ↔ y ∈ (minpoly K x).aroots S)
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C),
  CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl F =
    CategoryTheory.Limits.pushout.inr
      (CategoryTheory.Limits.coprod.desc
        (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.one))
        (F.map CategoryTheory.Limits.WalkingParallelPairHom.left))
      (CategoryTheory.Limits.coprod.desc
        (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.one))
        (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
-- Init.Data.Array.Lemmas
Array.flatMap_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → Array β} {x : α}, Array.flatMap f #[x] = f x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBlastCpopTreeTargetBlastCpopTree : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.limsup_add_bot_of_ne_top : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal},
  Filter.limsup u f = ⊥ → Filter.limsup v f ≠ ⊤ → Filter.limsup (u + v) f = ⊥
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_diagonal : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (a : n → α), (Matrix.diagonal a).diag = a
-- Mathlib.Data.Part
Part.div_mem_div : ∀ {α : Type u_1} [inst : Div α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma / mb ∈ a / b
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear : ∀ {R₀ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Ring S]
  [inst_3 : Algebra R₀ R] [inst_4 : Algebra R₀ S] (e : R ≃ₐ[R₀] S),
  CategoryTheory.Functor.Linear R₀ (ModuleCat.restrictScalarsEquivalenceOfRingEquiv e.toRingEquiv).functor
-- Init.Data.Vector.Lemmas
Vector.append_push : ∀ {α : Type u_1} {n m : ℕ} {as : Vector α n} {bs : Vector α m} {a : α}, as ++ bs.push a = (as ++ bs).push a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_union_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {fallback : β},
  Std.DTreeMap.Internal.Impl.contains k m₂ = false →
    Std.DTreeMap.Internal.Impl.Const.getD (m₁.union m₂ ⋯ ⋯) k fallback =
      Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.mk.inj : ∀ {carrier : Type u} {str : Monoid carrier} {carrier_1 : Type u} {str_1 : Monoid carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.GeometricallyIntegral.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.geometrically AlgebraicGeometry.IsIntegral f → AlgebraicGeometry.GeometricallyIntegral f
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.covarianceBilinDual.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} [inst_1 : NormedSpace ℝ E]
  [inst_2 : BorelSpace E] (μ : MeasureTheory.Measure E),
  ProbabilityTheory.covarianceBilinDual μ =
    ProbabilityTheory.uncenteredCovarianceBilinDual (MeasureTheory.Measure.map (fun x => x - ∫ (x : E), x ∂μ) μ)
-- Mathlib.Algebra.Module.Presentation.RestrictScalars
/-- The additional data that is necessary in order to obtain a presentation
of the restriction of scalars of a module.  -/
Module.Presentation.RestrictScalarsData : {B : Type u_1} →
  [inst : Ring B] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module B M] →
          [DecidableEq B] →
            (presM : Module.Presentation B M) →
              [DecidableEq presM.G] →
                {A : Type u_3} →
                  [inst_5 : CommRing A] →
                    [inst_6 : Algebra A B] → Module.Presentation A B → Type (max (max (max u_3 u_6) u_4) u_6 u_5)
-- Mathlib.Control.Monad.Cont
ContT.ext : ∀ {r : Type u} {m : Type u → Type v} {α : Type w} {x y : ContT r m α}, (∀ (f : α → m r), x.run f = y.run f) → x = y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₂ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.mk.sizeOf_spec : ∀ (inductiveVal : Lean.InductiveVal) (nminors : ℕ) (majorDecl : Lean.LocalDecl) (majorTypeFn : Lean.Expr)
  (majorTypeArgs majorTypeIndices : Array Lean.Expr),
  sizeOf
      { inductiveVal := inductiveVal, nminors := nminors, majorDecl := majorDecl, majorTypeFn := majorTypeFn,
        majorTypeArgs := majorTypeArgs, majorTypeIndices := majorTypeIndices } =
    1 + sizeOf inductiveVal + sizeOf nminors + sizeOf majorDecl + sizeOf majorTypeFn + sizeOf majorTypeArgs +
      sizeOf majorTypeIndices
-- Mathlib.RingTheory.Localization.Basic
/-- The localization at a module of units is isomorphic to the ring.  -/
IsLocalization.atUnits : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {S : Type u_2} →
        [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → M ≤ IsUnit.submonoid R → R ≃ₐ[R] S
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.iter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap α β), m.iter = m.inner.iter
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.weakEquivalences_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.weakEquivalences Cᵒᵖ = (HomotopicalAlgebra.weakEquivalences C).op
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
_private.Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex.0.SSet.Subcomplex.Pairing.RankFunction.isPushout_aux₃ : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] {j : ι},
  Function.Injective fun x =>
    { dim := x.dim,
      simplex := (CategoryTheory.ConcreteCategory.hom ((f.b j).app (Opposite.op { len := x.dim }))) x.simplex }
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformly.summable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {x : β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], SummableLocallyUniformly f → Summable fun x_1 => f x_1 x
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuous.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {z : Set β},
  LowerHemicontinuous fun _x => z
-- Mathlib.Algebra.Lie.Basic
LieEquiv.mk.inj : ∀ {R : Type u} {L : Type v} {L' : Type w} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : LieRing L'} {inst_4 : LieAlgebra R L'} {toLieHom : L →ₗ⁅R⁆ L'} {invFun : L' → L}
  {left_inv : autoParam (Function.LeftInverse invFun (↑toLieHom).toFun) LieEquiv.left_inv._autoParam}
  {right_inv : autoParam (Function.RightInverse invFun (↑toLieHom).toFun) LieEquiv.right_inv._autoParam}
  {toLieHom_1 : L →ₗ⁅R⁆ L'} {invFun_1 : L' → L}
  {left_inv_1 : autoParam (Function.LeftInverse invFun_1 (↑toLieHom_1).toFun) LieEquiv.left_inv._autoParam}
  {right_inv_1 : autoParam (Function.RightInverse invFun_1 (↑toLieHom_1).toFun) LieEquiv.right_inv._autoParam},
  { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toLieHom := toLieHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 } →
    toLieHom = toLieHom_1 ∧ invFun = invFun_1
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.hom_ext_iff : ∀ {X Y : FintypeCat} {f g : X ⟶ Y},
  f = g ↔
    ∀ (x : (fun X => X.obj) X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- Construct a `CommSemiring` instance expression from a `CommRing` instance expression  -/
Mathlib.Tactic.Determinant.commSemiringOfCommRing : {u : Lean.Level} → {α : Q(Type u)} → Q(CommRing «$α») → Q(CommSemiring «$α»)
-- Mathlib.Data.Prod.Basic
Prod.map_involutive : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {f : α → α} {g : β → β},
  Function.Involutive (Prod.map f g) ↔ Function.Involutive f ∧ Function.Involutive g
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Measure.restrict_singleton' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ] {a : α},
  μ.restrict {a} = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_getKey? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : (m.getKey? a).isSome = true}, (m.getKey? a).get h = m.getKey a ⋯
-- Mathlib.Analysis.Calculus.Deriv.Abs
DifferentiableWithinAt.abs_of_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E},
  DifferentiableWithinAt ℝ f s x → f x < 0 → DifferentiableWithinAt ℝ (fun x => |f x|) s x
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.Prod.containsIdentities : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [W₁.ContainsIdentities] [W₂.ContainsIdentities],
  (W₁.prod W₂).ContainsIdentities
-- Init.ShareCommon
ShareCommon.StateFactoryPointed : NonemptyType
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
deriv_arctan : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → deriv (fun x => Real.arctan (f x)) x = 1 / (1 + f x ^ 2) * deriv f x
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMon_map_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.LaxBraided] {X Y : CategoryTheory.CommMon C} (f : X ⟶ Y),
  (F.mapCommMon.map f).hom.hom = F.map f.hom.hom
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.borelMarkovFromReal_apply' : ∀ {α : Type u_1} {mα : MeasurableSpace α} (Ω : Type u_5) [inst : Nonempty Ω] [inst_1 : MeasurableSpace Ω]
  [inst_2 : StandardBorelSpace Ω] (η : ProbabilityTheory.Kernel α ℝ) (a : α) {s : Set Ω},
  MeasurableSet s →
    ((ProbabilityTheory.Kernel.borelMarkovFromReal Ω η) a) s =
      if (η a) (Set.range (MeasureTheory.embeddingReal Ω))ᶜ = 0 then (η a) (MeasureTheory.embeddingReal Ω '' s)
      else (MeasureTheory.embeddingReal Ω '' s).indicator 1 (Exists.choose ⋯)
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesColimit₂.isoObjCoconePointsOfIsColimit` w.r.t. the canonical maps to the colimit.  -/
CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoObjConePointsOfIsColimit_hom_assoc : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cocone K₁}
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone K₂}
  (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  {c₃ :
    CategoryTheory.Limits.Cocone
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))}
  (hc₃ : CategoryTheory.Limits.IsColimit c₃) (j : J₁ × J₂) {Z : C} (h : c₃.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((G.map (c₁.ι.app j.1)).app (K₂.obj j.2))
      (CategoryTheory.CategoryStruct.comp ((G.obj c₁.pt).map (c₂.ι.app j.2))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).hom h)) =
    CategoryTheory.CategoryStruct.comp (c₃.ι.app j) h
-- Mathlib.Algebra.Notation.Defs
dite_sub_dite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Sub α] (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α),
  ((if h : P then a h else b h) - if h : P then c h else d h) = if h : P then a h - c h else b h - d h
-- Mathlib.Data.Set.Monotone
strictMono_domRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMono (s.domRestrict f) ↔ StrictMonoOn f s
-- Mathlib.Analysis.Meromorphic.NormalForm
toMeromorphicNFAt_of_meromorphicOrderAt_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, meromorphicOrderAt f x ≠ 0 → toMeromorphicNFAt f x x = 0
-- Lean.Data.Lsp.Internal
/-- All declarations in `«namespace»` are opened, except for `exceptions`.  -/
Lean.Lsp.OpenNamespace.allExcept : Lean.Name → Array Lean.Name → Lean.Lsp.OpenNamespace
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix'_compLeft : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (B : LinearMap.BilinForm R₁ (n → R₁)) (f : (n → R₁) →ₗ[R₁] n → R₁),
  LinearMap.BilinForm.toMatrix' (B.compLeft f) = (LinearMap.toMatrix' f).transpose * LinearMap.BilinForm.toMatrix' B
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlDisplayProps.mk.inj : ∀ {html html_1 : ProofWidgets.Html}, { html := html } = { html := html_1 } → html = html_1
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.coe_doubleDualEquiv : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Finite α], ⇑AddChar.doubleDualEquiv = ⇑AddChar.doubleDualEmb
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A natural transformation `F ⟶ G` induces a natural transformation on
`Over X` up to `Over.map`.  -/
CategoryTheory.Over.postMap : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          {F G : CategoryTheory.Functor T D} →
            (e : F ⟶ G) →
              (CategoryTheory.Over.post F).comp (CategoryTheory.Over.map (e.app X)) ⟶ CategoryTheory.Over.post G
-- Mathlib.LinearAlgebra.DFinsupp
/-- If `DFinsupp.lsum` applied with `Submodule.subtype` is injective then the submodules are
iSupIndep.  -/
iSupIndep_of_dfinsupp_lsum_injective : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R N] (p : ι → Submodule R N),
  Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype) → iSupIndep p
-- Mathlib.Data.ZMod.Basic
ZMod.val_pos : ∀ {n : ℕ} {a : ZMod n}, 0 < a.val ↔ a ≠ 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.instFaithfulιHeart : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (H : Type u') [inst_6 : CategoryTheory.Category.{v', u'} H]
  [inst_7 : CategoryTheory.Preadditive H] [inst_8 : t.Heart H], t.ιHeart.Faithful
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.exists_exp_neg_natCast_lt_and_lt : ∀ {x y : WithZero (Multiplicative ℤ)}, x ≠ 0 → y ≠ 0 → ∃ k, WithZero.exp (-↑k) < x ∧ WithZero.exp (-↑k) < y
-- Mathlib.Data.PNat.Prime
PNat.exists_prime_and_dvd : ∀ {n : ℕ+}, n ≠ 1 → ∃ p, p.Prime ∧ p ∣ n
-- Init.Data.Array.Erase
Array.le_size_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, xs.size - 1 ≤ (xs.erase a).size
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.symm_bijective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Function.Bijective FirstOrder.Language.PartialEquiv.symm
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_abs_left`. -/
Asymptotics.IsLittleO.abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
  u =o[l] g → (fun x => |u x|) =o[l] g
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Abelian C] {ι' : Type u_3}
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (n₀ : ℤ) (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁)
  (h₁₂ : i₁ ≤ i₂),
  CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁))) →
    CategoryTheory.Mono ((X'.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.dropPrefix?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (head : α) (tail : List α)
  (h_1 : (list : List α) → motive list []) (h_2 : (head : α) → (tail : List α) → motive [] (head :: tail))
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match [], head :: tail with
    | list, [] => h_1 list
    | [], head :: tail => h_2 head tail
    | a :: as, b :: bs => h_3 a as b bs) =
    h_2 head tail
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] ⦃f g : MeasureTheory.SimpleFunc α β⦄, ⇑f = ⇑g → f = g
-- Mathlib.Order.CompleteLattice.Basic
Function.Surjective.iInf_comp : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : InfSet α] {f : ι → ι'},
  Function.Surjective f → ∀ (g : ι' → α), ⨅ x, g (f x) = ⨅ y, g y
-- Mathlib.Tactic.GRewrite.Core
/-- When `implicationHyp = true`, interpret the rewrite rule as an implication.  -/
Mathlib.Tactic.GRewrite.Config.implicationHyp : Mathlib.Tactic.GRewrite.Config → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  CategoryTheory.Limits.PreservesPullback.iso G f g = CategoryTheory.Limits.PreservesPullback.iso G f g
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))),
  (s.reindex e).exradius signs = s.exradius (Finset.map e.symm.toEmbedding signs)
-- Mathlib.Data.Nat.Choose.Factorization
Nat.factorization_choose_prime_pow_add_factorization : ∀ {p n k : ℕ}, Nat.Prime p → k ≤ p ^ n → k ≠ 0 → ((p ^ n).choose k).factorization p + k.factorization p = n
-- Init.Data.Array.Lex.Lemmas
Array.map_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [Std.Asymm fun x1 x2 => x1 < x2]
  [Std.Trichotomous fun x1 x2 => x1 < x2] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {xs ys : Array α} {f : α → β}, (∀ (x y : α), x < y → f x < f y) → xs ≤ ys → Array.map f xs ≤ Array.map f ys
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.factorThruImage_comp_imageUnopOp_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage g) (CategoryTheory.imageUnopOp g).inv =
    (CategoryTheory.Limits.image.ι g.unop).op
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.mul_left : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {f g : MvPowerSeries τ R},
  PowerSeries.HasSubst f → PowerSeries.HasSubst (f * g)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instInv.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : ContinuousInv G],
  SeparationQuotient.instInv = { inv := Quotient.map' (fun x => x⁻¹) ⋯ }
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Product of a list of elements in a submonoid is in the submonoid.  -/
list_prod_mem : ∀ {M : Type u_1} {B : Type u_3} [inst : Monoid M] [inst_1 : SetLike B M] [SubmonoidClass B M] {S : B} {l : List M},
  (∀ x ∈ l, x ∈ S) → l.prod ∈ S