mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Order
/-- **Alias** of `AnalyticOnNhd.codiscrete_setOfPred_analyticOrderAt_eq_zero_or_top`.

---

The set where an analytic function has zero or infinite order is discrete within its domain of
analyticity.  -/
AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  AnalyticOnNhd 𝕜 f U → {u | analyticOrderAt f ↑u = 0 ∨ analyticOrderAt f ↑u = ⊤} ∈ Filter.codiscrete ↑U
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : AddCommMonoid X] [inst_1 : AddCommMonoid Y] (f : X →+ Y),
  AddCommMonCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_toList_rco : ∀ {m n : ℤ}, (m<...=n).toList = ((m + 1)...n + 1).toList
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- A homological complex `K` is exact at `i` if the short complex `K.sc i` is exact.  -/
HomologicalComplex.ExactAt : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → HomologicalComplex C c → ι → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The image of a pullback cone by a functor.  -/
CategoryTheory.Limits.PushoutCocone.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {W X Y : C} →
          {f : W ⟶ X} →
            {g : W ⟶ Y} →
              CategoryTheory.Limits.PushoutCocone f g →
                (G : CategoryTheory.Functor C D) → CategoryTheory.Limits.PushoutCocone (G.map f) (G.map g)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_hom_left_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : R.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom T.hom) S.hom))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) h)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.mem_uIcc_of_le : ∀ {α : Type u_1} [inst : Lattice α] {a b x : α}, a ≤ x → x ≤ b → x ∈ Set.uIcc a b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_alter_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  ¬cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ k' ∈ t)
-- Lean.Meta.Basic
Lean.Meta.instBEqInfoCacheKey : BEq Lean.Meta.InfoCacheKey
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPrecompProperty : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasTwoOutOfThreeProperty], W.HasOfPrecompProperty W
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.equivElements_apply_snd : ∀ {X : SSet} (s : X.S), (SSet.S.equivElements s).snd = s.simplex
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_mapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {n : Type w → Type w''}
  {f : β → Std.Iterators.PostconditionT n γ} [inst_1 : Monad n] [LawfulMonad n],
  (Std.Iter.mapWithPostcondition f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => do
      let out' ← (f out).operation
      pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.Iter.mapWithPostcondition f it') ↑out' ⋯))
    | ⟨Std.IterStep.skip it', h⟩ =>
      pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.mapWithPostcondition f it') ⋯))
    | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_nonpos_of_ae : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X},
  f ≤ᵐ[μ] 0 → ∫ (x : X) in s, f x ∂μ ≤ 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `LawfulOrderLT` instance if available  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.lawfulOrderLTInst? : Lean.Meta.Grind.Arith.Linear.NatStruct → Option Lean.Expr
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.hasForgetToAddMonCat.eq_1 : AddGrpCat.hasForgetToAddMonCat =
  {
    forget₂ :=
      { obj := fun X => AddMonCat.of ↑X, map := fun {X Y} f => AddMonCat.ofHom (AddGrpCat.Hom.hom f),
        map_id := AddGrpCat.hasForgetToAddMonCat._proof_1, map_comp := @AddGrpCat.hasForgetToAddMonCat._proof_2 },
    forget_comp := AddGrpCat.hasForgetToAddMonCat._proof_4 }
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.induction_on : ∀ {m : ℤ} {C : FixedDetMatrix (Fin 2) ℤ m → Prop} {A : FixedDetMatrix (Fin 2) ℤ m},
  m ≠ 0 →
    (∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A) →
      (∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.S • B)) →
        (∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.T • B)) → C A
-- Mathlib.Order.SymmDiff
symmDiff_right_involutive : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a : α), Function.Involutive fun x => symmDiff a x
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.bijective_iff_isIso_ofHom : ∀ {X Y : Type u} (f : X → Y), Function.Bijective f ↔ CategoryTheory.IsIso (TypeCat.ofHom f)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.pre_obj_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C)
  (X : CategoryTheory.Grothendieck (G.comp F)), ((CategoryTheory.Grothendieck.pre F G).obj X).fiber = X.fiber
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- Fixing submonoid of iUnion is intersection  -/
fixingSubmonoid_iUnion : ∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α] {ι : Sort u_3} {s : ι → Set α},
  fixingSubmonoid M (⋃ i, s i) = ⨅ i, fixingSubmonoid M (s i)
-- Mathlib.Algebra.Category.Grp.Ulift
GrpCat.uliftFunctor_preservesLimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J GrpCat),
  CategoryTheory.Limits.PreservesLimit K GrpCat.uliftFunctor
-- Batteries.Recycling.RBTree.WF
/-- A `red` node with the red-red invariant has balanced children.  -/
RBTree.RBNode.RedRed.of_red : ∀ {p : Prop} {α : Type u_1} {a : RBTree.RBNode α} {x : α} {b : RBTree.RBNode α} {n : ℕ},
  RBTree.RBNode.RedRed p (RBTree.RBNode.node RBTree.RBColor.red a x b) n → ∃ c₁ c₂, a.Balanced c₁ n ∧ b.Balanced c₂ n
-- Mathlib.Algebra.Group.Subgroup.Even
Subsemigroup.square.eq_1 : ∀ (S : Type u_1) [inst : CommSemigroup S], Subsemigroup.square S = { carrier := {s | IsSquare s}, mul_mem' := ⋯ }
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side.  -/
Orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).sin * ‖x + y‖ = ‖x‖
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- `localized₀` is the same as `localized'` considered as a submodule over the base ring.  -/
Submodule.restrictScalars_localized' : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (M' : Submodule R M),
  Submodule.restrictScalars R (Submodule.localized' S p f M') = Submodule.localized₀ p f M'
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
          Z)
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y
            Z).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv : ∀ (𝕜 : Type u_2) {𝕜' : Type u_3} {D : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜]
  [inst_5 : NormedAddCommGroup D] [inst_6 : NormedSpace ℝ D] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : NontriviallyNormedField 𝕜'] [inst_9 : NormedAlgebra ℝ 𝕜'] [inst_10 : NormedSpace 𝕜' F] {u : D → 𝕜'},
  Function.HasTemperateGrowth u →
    ∀ (g : D ≃L[ℝ] E) (f : SchwartzMap E F),
      (SchwartzMap.smulLeftCLM F u) ((SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g) f) =
        (SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g) ((SchwartzMap.smulLeftCLM F (u ∘ ⇑g.symm)) f)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.extractAndExtendAux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : 0 = 0 → motive 0) (h_2 : (n' : ℕ) → 0 = n'.succ → motive n'.succ),
  (match hwi : 0 with
    | 0 => h_1 hwi
    | n'.succ => h_2 n' hwi) =
    h_1 ⋯
-- Init.Data.Vector.Lex
Vector.instIsLinearOrderOfLawfulOrderLT : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α],
  Std.IsLinearOrder (Vector α n)
-- Lean.Meta.Match.Match
/-- Create a dependent matcher for `matchType` where `matchType` is of the form
`(a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> B[a_1, ..., a_n]`
where `n = numDiscrs`, and the `lhss` are the left-hand-sides of the `match`-expression alternatives.
Each `AltLHS` has a list of local declarations and a list of patterns.
The number of patterns must be the same in each `AltLHS`.
The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
`(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
 -/
Lean.Meta.Match.mkMatcher : Lean.Meta.Match.MkMatcherInput → Lean.MetaM Lean.Meta.Match.MatcherResult
-- Mathlib.NumberTheory.Zsqrtd.Basic
_private.Mathlib.NumberTheory.Zsqrtd.Basic.0.Zsqrtd.Nonneg.match_1.splitter : {d : ℕ} → (motive : ℤ√↑d → Sort u_1) → (x : ℤ√↑d) → ((a b : ℤ) → motive { re := a, im := b }) → motive x
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.lintegral_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ]
  {f : α × β → ENNReal}, Measurable f → ∫⁻ (x : α × β), f x ∂μ.compProd κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
LiouvilleNumber.summable : ∀ {m : ℝ}, 1 < m → Summable fun i => 1 / m ^ i.factorial
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If two sets coincide locally, except maybe at a point, then derivatives within these sets
are the same.  -/
mfderivWithin_congr_set' : ∀ {𝕜 : 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}
  (y : M), s =ᶠ[nhdsWithin x {y}ᶜ] t → mfderiv[s] f x = mfderiv[t] f x
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.left_vsub_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), p₀ -ᵥ (AffineMap.lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.hasBasis_nhds_one_of_basis : ∀ {α : Type u_1} {G : Type u_2} {ι : Type u_3} [inst : Group G] [inst_1 : UniformSpace G] [IsUniformGroup G]
  (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ {p : ι → Prop} {b : ι → Set G},
        (nhds 1).HasBasis p b →
          (nhds 1).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
            {f | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}
-- Mathlib.RingTheory.DividedPowers.Basic
dividedPowersBot.eq_1 : ∀ (A : Type u_1) [inst : CommSemiring A],
  dividedPowersBot A =
    { dpow := fun n a => if a = 0 ∧ n = 0 then 1 else 0, dpow_null := ⋯, dpow_zero := ⋯, dpow_one := ⋯, dpow_mem := ⋯,
      dpow_add := ⋯, dpow_mul := ⋯, mul_dpow := ⋯, dpow_comp := ⋯ }
-- Mathlib.Order.UpperLower.Closure
instDecidablePredMemUpperClosure : {α : Type u_1} →
  [inst : Preorder α] →
    {s : Set α} → [DecidablePred fun x => ∃ a ∈ s, a ≤ x] → DecidablePred fun x => x ∈ upperClosure s
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.zero_anti : ∀ {α : Type u_5} {β : Type u_6} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Zero β], Antitone 0
-- Mathlib.Algebra.Group.Defs
/-- Subtracting an element is the same as adding by its negative.
This is a duplicate of `SubNegMonoid.sub_eq_add_neg` ensuring that the types unfold better.  -/
sub_eq_add_neg : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a b : G), a - b = a + -b
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_sub : ∀ (a b : BitVec 64), Int64.ofBitVec (a - b) = Int64.ofBitVec a - Int64.ofBitVec b
-- Batteries.Data.PairingHeap
/-- The well formedness predicate for a pairing heap.
It asserts that:
* There is no more than one tree.
* It is a `le`-min-heap (if `le` is well-behaved)
 -/
Batteries.PairingHeapImp.Heap.WF : {α : Type u_1} → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → Prop
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.smul_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} {G : Type u_4} [inst_1 : (i : ι) → SMul G (R i)] [inst_2 : ∀ (i : ι), SMulMemClass (S i) G (R i)]
  (g : G) (x : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), (g • x) i = g • x i
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If `x` is isolated in `s`, then `f` has any derivative at `x` within `s`,
as this statement is empty.  -/
HasFDerivWithinAt.of_not_accPt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  ¬AccPt x (Filter.principal s) → HasFDerivWithinAt f f' s x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.mk.injEq : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (toMonoidHom : A →* B)
  (continuous_toFun : autoParam (Continuous (↑toMonoidHom).toFun) ContinuousMap.continuous_toFun._autoParam)
  (toMonoidHom_1 : A →* B)
  (continuous_toFun_1 : autoParam (Continuous (↑toMonoidHom_1).toFun) ContinuousMap.continuous_toFun._autoParam),
  ({ toMonoidHom := toMonoidHom, continuous_toFun := continuous_toFun } =
      { toMonoidHom := toMonoidHom_1, continuous_toFun := continuous_toFun_1 }) =
    (toMonoidHom = toMonoidHom_1)
-- Init.Data.Fin.Lemmas
Fin.reverseInduction.eq_1 : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (last : motive (Fin.last n))
  (cast : (i : Fin n) → motive i.succ → motive i.castSucc) (i : Fin (n + 1)),
  Fin.reverseInduction last cast i = Fin.reverseInduction.go cast i n ⋯ ⋯ last
-- Mathlib.Algebra.Exact.Basic
/-- When we have a commutative diagram from a sequence of two maps to another,
such that the left vertical map is surjective, the middle vertical map is bijective and the right
vertical map is injective, then the upper row is exact iff the lower row is.
See `ShortComplex.exact_iff_of_epi_of_isIso_of_mono` in the file
`Mathlib/Algebra/Homology/ShortComplex/Exact.lean` for the categorical version of this result.  -/
AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective : ∀ {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} {N₃ : Type u_13}
  [inst : AddCommMonoid M₁] [inst_1 : AddCommMonoid M₂] [inst_2 : AddCommMonoid M₃] [inst_3 : AddCommMonoid N₁]
  [inst_4 : AddCommMonoid N₂] [inst_5 : AddCommMonoid N₃] (f : M₁ →+ M₂) (g : M₂ →+ M₃) (f' : N₁ →+ N₂) (g' : N₂ →+ N₃)
  (τ₁ : M₁ →+ N₁) (τ₂ : M₂ →+ N₂) (τ₃ : M₃ →+ N₃),
  f'.comp τ₁ = τ₂.comp f →
    g'.comp τ₂ = τ₃.comp g →
      Function.Surjective ⇑τ₁ →
        Function.Bijective ⇑τ₂ → Function.Injective ⇑τ₃ → (Function.Exact ⇑f ⇑g ↔ Function.Exact ⇑f' ⇑g')
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_le_add_iff_right : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [inst_1 : LE α] [AddRightMono α] [AddRightReflectLE α],
  z ≠ ⊥ → (x + z ≤ y + z ↔ x ≤ y)
-- Mathlib.Topology.Algebra.Group.Basic
/-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of `1`
such that `K * V ⊆ U`.  -/
compact_open_separated_mul_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : MulOneClass G] [ContinuousMul G] {K U : Set G},
  IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 1, K * V ⊆ U
-- Mathlib.Topology.KrullDimension
topologicalKrullDim_zero_of_discreteTopology : ∀ (X : Type u_3) [inst : TopologicalSpace X] [DiscreteTopology X], topologicalKrullDim X ≤ 0
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- The bornology on `Unitization 𝕜 A` is inherited from `𝕜 × A`.  -/
Unitization.instBornology : {𝕜 : Type u_1} → {A : Type u_2} → [NontriviallyNormedField 𝕜] → [NonUnitalNormedRing A] → Bornology (Unitization 𝕜 A)
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instBEqBodyState : BEq Std.Http.Protocol.H1.Reader.BodyState
-- Mathlib.Control.Bifunctor
Bifunctor.bimap : {F : Type u₀ → Type u₁ → Type u₂} →
  [self : Bifunctor F] → {α α' : Type u₀} → {β β' : Type u₁} → (α → α') → (β → β') → F α β → F α' β'
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.hasMFDerivWithinAt_symm : ∀ {𝕜 : 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) {x : E},
  x ∈ Set.range ↑I →
    HasMFDerivAt[Set.range ↑I] (↑I.symm) x (ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) x))
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_lt : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, s.erase a < s ↔ a ∈ s
-- Mathlib.RingTheory.PicardGroup
LinearEquiv.conj.eq_1 : ∀ {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [inst : CommSemiring R₁']
  [inst_1 : CommSemiring R₂'] [inst_2 : AddCommMonoid M₁'] [inst_3 : AddCommMonoid M₂'] [inst_4 : Module R₁' M₁']
  [inst_5 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [inst_6 : RingHomInvPair σ₁'₂' σ₂'₁']
  [inst_7 : RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂'), e.conj = e.arrowCongr e
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_symm_apply : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (h : G'.IsSpanning) (v : ↑G'.verts),
  (RelIso.symm (G'.spanningCoeEquivCoeOfSpanning h)) v = ↑v
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_eq_some_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.minKey? = some (t.minKeyD fallback)
-- Mathlib.RingTheory.Perfection
Perfection.coeff_iterate_frobenius' : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (f : Perfection R p)
  (n m : ℕ),
  m ≤ n → (Perfection.coeff R p n) ((⇑(frobenius (Perfection R p) p))^[m] f) = (Perfection.coeff R p (n - m)) f
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing.inj : ∀ {id id_1 : ℕ},
  Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing id = Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing id_1 → id = id_1
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
/-- Isometric equivalences are isometric maps  -/
LinearMap.BilinForm.IsometryEquiv.toIsometry : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} → {B₂ : LinearMap.BilinForm R M₂} → B₁.IsometryEquiv B₂ → B₁ →bᵢ B₂
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.isDenseInducing_toCompl : ∀ (α : Type u_3) [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α],
  IsDenseInducing ⇑UniformSpace.Completion.toCompl
-- Qq.SortLocalDecls
Qq.SortLocalDecls.Context.localDecls : Qq.SortLocalDecls.Context → Lean.NameMap Lean.LocalDecl
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.mk : ∀ {S : Type u_3} {M : outParam (Type u_4)} [inst : Add M] [inst_1 : SetLike S M],
  (∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) → AddMemClass S M
-- Mathlib.Algebra.Category.ModuleCat.Abelian
ModuleCat.forget₂_reflectsLimits : ∀ {R : Type u} [inst : Ring R],
  CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Month.Offset` to a `PlainDateTime`, adjusting the day to the last valid day of the resulting
month.
 -/
Std.Time.PlainDateTime.addMonthsClip : Std.Time.PlainDateTime → Std.Time.Month.Offset → Std.Time.PlainDateTime
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Hom.toOrderHom_mk : ∀ {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)), (SimplexCategory.Hom.mk f).toOrderHom = f
-- Mathlib.Analysis.Convex.BetweenList
List.sbtw_triple : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {p₁ p₂ p₃ : P},
  List.Sbtw R [p₁, p₂, p₃] ↔ Sbtw R p₁ p₂ p₃