mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_flip : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} (xs : List.Vector α n)
  (ys : List.Vector β n) (f : α → β → σ → σ × γ),
  List.Vector.mapAccumr₂ f xs ys s = List.Vector.mapAccumr₂ (flip f) ys xs s
-- Mathlib.Data.Stream.Defs
/-- Zip two streams using a binary operation:
`Stream'.get n (Stream'.zip f s₁ s₂) = f (Stream'.get s₁) (Stream'.get s₂)`.  -/
Stream'.zip : {α : Type u} → {β : Type v} → {δ : Type w} → (α → β → δ) → Stream' α → Stream' β → Stream' δ
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.desc.multicofork_π_zero_assoc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃)
  {Z : SSet} (h : (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨0, SSet.horn₃₁.desc.multicofork_π_zero._proof_1⟩) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 0).inv f₀) h
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.compLeft.eq_1 : ∀ {α : Type u_5} {β : Type u_6} [inst : Add α] [inst_1 : Add β] (f : α →ₙ+ β) (I : Type u_7),
  f.compLeft I = { toFun := fun h => ⇑f ∘ h, map_add' := ⋯ }
-- Mathlib.SetTheory.Cardinal.Arithmetic
/-- If `α` is an infinite type, then `α ⊕ α` and `α` have the same cardinality.  -/
Cardinal.add_eq_self : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c + c = c
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.withoutHeedElabAsElimImp : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Init.Data.List.Scan.Lemmas
List.scanlM_pure : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] [LawfulMonad m] {f : β → α → β}
  {as : List α}, List.scanlM (fun x1 x2 => pure (f x1 x2)) init as = pure (List.scanl f init as)
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.somePath_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y) (t : ↑unitInterval),
  h.somePath t ∈ F
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.asEmptyCone_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (X_1 : CategoryTheory.Discrete PEmpty.{1}),
  (CategoryTheory.Limits.asEmptyCone X).π.app X_1 = id (CategoryTheory.Discrete.casesOn X_1 fun as => ⋯.elim)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.mu_naturality : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) ⦃X Y : C⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (T.map (T.map f)) (T.μ.app Y) =
    CategoryTheory.CategoryStruct.comp (T.μ.app X) (T.map f)
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- When `[WellPowered C] [HasImages C] [HasCoproducts C]`,
`Subobject A` has arbitrary supremums.  -/
CategoryTheory.Subobject.sSup : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        [CategoryTheory.Limits.HasCoproducts C] →
          [CategoryTheory.Limits.HasImages C] → {A : C} → Set (CategoryTheory.Subobject A) → CategoryTheory.Subobject A
-- Init.Data.Int.Order
Int.le_of_neg_le_neg : ∀ {a b : ℤ}, -b ≤ -a → a ≤ b
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- An equivalence between an `IsKleinFour` group `G₁` and a group `G₂` of exponent two which sends
`1 : G₁` to `1 : G₂` is in fact an isomorphism.  -/
IsKleinFour.mulEquiv' : {G₁ : Type u_2} →
  {G₂ : Type u_3} →
    [inst : Group G₁] →
      [inst_1 : Group G₂] → [IsKleinFour G₁] → (e : G₁ ≃ G₂) → e 1 = 1 → Monoid.exponent G₂ = 2 → G₁ ≃* G₂
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- The map from the quotient of `M` by submodule `p` to the quotient of `M₂` by submodule `q` along
`f : M → M₂` is linear.  -/
Submodule.mapQ : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (p : Submodule R M) →
            {R₂ : Type u_3} →
              {M₂ : Type u_4} →
                [inst_3 : Ring R₂] →
                  [inst_4 : AddCommGroup M₂] →
                    [inst_5 : Module R₂ M₂] →
                      {τ₁₂ : R →+* R₂} →
                        (q : Submodule R₂ M₂) → (f : M →ₛₗ[τ₁₂] M₂) → p ≤ Submodule.comap f q → M ⧸ p →ₛₗ[τ₁₂] M₂ ⧸ q
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
/-- A function which is `EventuallyEq` to some `Measurable` function is `EventuallyMeasurable`.  -/
Measurable.eventuallyMeasurable_of_eventuallyEq : ∀ {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [inst : CountableInterFilter l] {β : Type u_2}
  [inst_1 : MeasurableSpace β] {f g : α → β}, Measurable f → g =ᶠ[l] f → EventuallyMeasurable m l g
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl : ∀ {R : Type u} [inst : CommRing R] (s : TopologicalSpace.Clopens (PrimeSpectrum R)),
  PrimeSpectrum.isIdempotentElemEquivClopens.symm sᶜ = ⟨1 - ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s), ⋯⟩
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.instCommMonoid : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              (x : Submonoid A) →
                [inst_3 : AddCommMonoid ι] →
                  [inst_4 : DecidableEq ι] → [GradedRing 𝒜] → CommMonoid (HomogeneousLocalization.NumDenSameDeg 𝒜 x)
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.hasSum_inl : ∀ {α : Type u_1} {R : Type u_3} (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid R] [inst_3 : AddCommMonoid M] {f : α → R} {a : R},
  HasSum f a → HasSum (fun x => TrivSqZeroExt.inl (f x)) (TrivSqZeroExt.inl a)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.equivPair.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (i : ι),
  Monoid.PushoutI.NormalWord.equivPair i =
    {
      toFun := fun w =>
        { toPair := (Monoid.CoprodI.Word.equivPair i) (Monoid.CoprodI.of ((φ i) w.head) • w.toWord), normalized := ⋯ },
      invFun := Monoid.PushoutI.NormalWord.rcons i, left_inv := ⋯, right_inv := ⋯ }
-- Lean.Setup
Lean.instReprModuleHeader.repr : Lean.ModuleHeader → ℕ → Std.Format
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.versoSyntaxToString' : Lean.Syntax → ReaderT ℕ (StateM String) Unit
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.mk.injEq : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (setsAt : X → Set (Set X)) (measurableSet : ∀ (x : X), ∀ s ∈ setsAt x, MeasurableSet s)
  (nonempty_interior : ∀ (x : X), ∀ s ∈ setsAt x, (interior s).Nonempty)
  (nontrivial : ∀ (x : X), ∀ ε > 0, ∃ s ∈ setsAt x, s ⊆ Metric.closedBall x ε)
  (covering :
    ∀ (s : Set X) (f : X → Set (Set X)),
      (∀ x ∈ s, f x ⊆ setsAt x) →
        (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
          ∃ t,
            (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0)
  (setsAt_1 : X → Set (Set X)) (measurableSet_1 : ∀ (x : X), ∀ s ∈ setsAt_1 x, MeasurableSet s)
  (nonempty_interior_1 : ∀ (x : X), ∀ s ∈ setsAt_1 x, (interior s).Nonempty)
  (nontrivial_1 : ∀ (x : X), ∀ ε > 0, ∃ s ∈ setsAt_1 x, s ⊆ Metric.closedBall x ε)
  (covering_1 :
    ∀ (s : Set X) (f : X → Set (Set X)),
      (∀ x ∈ s, f x ⊆ setsAt_1 x) →
        (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
          ∃ t,
            (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0),
  ({ setsAt := setsAt, measurableSet := measurableSet, nonempty_interior := nonempty_interior, nontrivial := nontrivial,
        covering := covering } =
      { setsAt := setsAt_1, measurableSet := measurableSet_1, nonempty_interior := nonempty_interior_1,
        nontrivial := nontrivial_1, covering := covering_1 }) =
    (setsAt = setsAt_1)
-- Mathlib.Control.Traversable.Lemmas
Traversable.naturality_pf : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F G : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] [inst_4 : Applicative G] [LawfulApplicative G] {α β : Type u}
  (η : ApplicativeTransformation F G) (f : α → F β),
  traverse ((fun {α} => η.app α) ∘ f) = (fun {α} => η.app α) ∘ traverse f
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.map₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} [inst : Zero β] [inst_1 : Zero γ]
  {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α β} [inst_2 : Zero δ],
  f.FinMeasSupp μ →
    ∀ {g : MeasureTheory.SimpleFunc α γ},
      g.FinMeasSupp μ →
        ∀ {op : β → γ → δ}, op 0 0 = 0 → (MeasureTheory.SimpleFunc.map (Function.uncurry op) (f.pair g)).FinMeasSupp μ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} {aig : Std.Sat.AIG α} {w : ℕ}
  (input input_1 : aig.RefVec w),
  input = input_1 →
    ∀ (start start_1 : ℕ),
      start = start_1 →
        ∀ (curr : ℕ) (hcurr : curr ≤ newWidth) (s s_1 : aig.RefVec curr),
          s = s_1 →
            Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go input start curr hcurr s =
              Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go input_1 start_1 curr hcurr s_1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Localization.mulEquivOfQuotient_symm_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (x : M) (y : ↥S),
  (Localization.mulEquivOfQuotient f).symm (f.mk' x y) = (Localization.monoidOf S).mk' x y
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.liftWith_OptionT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  (f : ({β : Type u} → OptionT m β → m (Option β)) → m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp (f fun {β} x => x.run) post epost.tail ⦄ MonadControl.liftWith f ⦃ post; epost ⦄
-- Mathlib.Logic.Equiv.Defs
/-- `Prop` is noncomputably equivalent to `Bool`.  -/
Equiv.propEquivBool : Prop ≃ Bool
-- Mathlib.Algebra.Homology.Localization
HomotopyCategory.quasiIso.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C] ⦃X Y : HomotopyCategory C c⦄
  (x x_1 : X ⟶ Y), x = x_1 → HomotopyCategory.quasiIso C c x = HomotopyCategory.quasiIso C c x_1
-- Mathlib.MeasureTheory.Measure.Portmanteau
MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
  {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω},
  MeasurableSet E → μ Eᶜ ≤ Filter.liminf (fun i => (μs i) Eᶜ) L → Filter.limsup (fun i => (μs i) E) L ≤ μ E
-- Mathlib.GroupTheory.Divisible
/-- Any quotient group of a divisible group is divisible  -/
QuotientAddGroup.divisibleBy : {A : Type u_2} → [inst : AddCommGroup A] → (B : AddSubgroup A) → [DivisibleBy A ℕ] → DivisibleBy (A ⧸ B) ℕ
-- Mathlib.Algebra.Order.Group.Defs
neg_neg_of_pos : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a : α}, 0 < a → -a < 0
-- Mathlib.Data.PFun
PFun.prodMap_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β),
  f.prodMap g x = { Dom := (f x.1).Dom ∧ (g x.2).Dom, get := fun h => ((f x.1).get ⋯, (g x.2).get ⋯) }
-- Mathlib.Data.Set.Image
/-- If the image of a set under an injective map is a subsingleton, the set is a subsingleton.  -/
Set.subsingleton_of_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → ∀ (s : Set α), (f '' s).Subsingleton → s.Subsingleton
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.nextCoeffUp_of_constantCoeff_eq_zero : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.coeff 0 = 0 → p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R) =
    CategoryTheory.ChosenPullbacksAlong.pullbackMap T.hom R.hom S.hom R.hom (CategoryTheory.Over.Hom.left f)
      (CategoryTheory.CategoryStruct.id R.left) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
-- Mathlib.Data.PNat.Prime
PNat.gcd_eq_right_iff_dvd : ∀ {m n : ℕ+}, n.gcd m = m ↔ m ∣ n
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_id : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)], (DirectSum.lmap fun i => LinearMap.id) = LinearMap.id
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_eq_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {k fallback : α},
  m.contains k = true → m.getD k fallback = k
-- Mathlib.Logic.Function.Defs
Function.prod_comp_prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : ι → α) (g : ι → β) {γ : Type u_4} {δ : Type u_5} (h : α × β → γ)
  (k : α × β → δ), Function.prod h k ∘ Function.prod f g = Function.prod (h ∘ Function.prod f g) (k ∘ Function.prod f g)
-- Mathlib.Data.Prod.TProd
/-- A version of `TProd.elim` when `l` contains all elements. In this case we get a function into
`Π i, α i`.  -/
List.TProd.elim' : {ι : Type u} → {α : ι → Type v} → {l : List ι} → [DecidableEq ι] → (∀ (i : ι), i ∈ l) → List.TProd α l → (i : ι) → α i
-- Mathlib.Algebra.CubicDiscriminant
Cubic.ne_zero_of_b_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.b ≠ 0 → P.toPoly ≠ 0
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.multisetProd_one : ∀ {n : ℤ} {s : Multiset ℤ}, (∀ x ∈ s, x ≡ 1 [ZMOD n]) → s.prod ≡ 1 [ZMOD n]
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Ideal.isDomain : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A], IsDomain (Ideal A)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMul_assoc : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} {q : Type u_13} {r : Type u_14} [inst : CommSemiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : AddCommMonoid β] [inst_3 : AddCommMonoid γ] [inst_4 : Module R α] [inst_5 : Module R β]
  [inst_6 : Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ),
  (Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r))
      ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map
        ⇑(TensorProduct.assoc R α β γ)) =
    Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_get? : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.LawfulEqOrd α]
  [Std.TransOrd α], t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.Const.get? t a = t.get? a
-- Mathlib.Data.Int.Init
Int.leInduction.eq_1 : ∀ {m : ℤ} {motive : (n : ℤ) → m ≤ n → Sort u_1} (base : motive m ⋯)
  (succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯) (n : ℤ),
  Int.leInduction base succ n =
    Int.inductionOn' (motive := fun x => (hmn : m ≤ x) → motive x hmn) n m (fun x => base)
      (fun k hle ih x => succ k hle (ih hle)) fun x x_1 x_2 x_3 => ⋯.elim
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.wideCospan_map : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C)
  (arrows : (j : J) → objs j ⟶ B) {X Y : CategoryTheory.Limits.WidePullbackShape J} (f : X ⟶ Y),
  (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows).map f =
    CategoryTheory.Limits.WidePullbackShape.Hom.casesOn (motive := fun a a_1 x =>
      X = a → Y = a_1 → f ≍ x → (Option.casesOn X B objs ⟶ Option.casesOn Y B objs)) f
      (fun X_1 h =>
        Eq.ndrec (motive := fun X_2 =>
          Y = X_2 →
            f ≍ CategoryTheory.Limits.WidePullbackShape.Hom.id X_2 →
              (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
          (fun h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : X ⟶ Y) →
                f ≍ CategoryTheory.Limits.WidePullbackShape.Hom.id X →
                  (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
              (fun f h => CategoryTheory.CategoryStruct.id (Option.casesOn X B objs)) ⋯ f)
          h)
      (fun j h =>
        Eq.ndrec (motive := fun {X} =>
          (f : X ⟶ Y) →
            Y = none →
              f ≍ CategoryTheory.Limits.WidePullbackShape.Hom.term j →
                (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : some j ⟶ Y) →
                f ≍ CategoryTheory.Limits.WidePullbackShape.Hom.term j →
                  (Option.casesOn (some j) B objs ⟶ Option.casesOn Y B objs))
              (fun f h => arrows j) ⋯ f)
          ⋯ f)
      ⋯ ⋯ ⋯
-- Mathlib.NumberTheory.ModularForms.Discriminant
ModularForm.eta.eq_1 : ∀ (z : ℂ), ModularForm.eta z = Function.Periodic.qParam 24 z * ∏' (n : ℕ), (1 - ModularForm.eta_q n z)
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.liftOn_mk : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : Sort v} (p q : Polynomial K)
  (f : Polynomial K → Polynomial K → P),
  (∀ (p : Polynomial K), f p 0 = f 0 1) →
    ∀ (H' : ∀ {p q p' q' : Polynomial K}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q')
      (H :
        optParam
          (∀ {p q p' q' : Polynomial K},
            q ∈ nonZeroDivisors (Polynomial K) →
              q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q')
          ⋯),
      (RatFunc.mk p q).liftOn f H = f p q
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- Rank functions for `h : A.PairingCore` correspond to
rank functions for `h.pairing : A.Pairing`.  -/
SSet.Subcomplex.PairingCore.rankFunctionEquiv : {X : SSet} →
  {A : X.Subcomplex} →
    (h : A.PairingCore) → (α : Type v) → [inst : PartialOrder α] → h.RankFunction α ≃ h.pairing.RankFunction α
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the second morphism of a triangle  -/
CategoryTheory.Pretriangulated.Triangle.mor₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → (self : CategoryTheory.Pretriangulated.Triangle C) → self.obj₂ ⟶ self.obj₃
-- Mathlib.Condensed.Discrete.Colimit
Condensed.finYoneda_map : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) {X Y : FintypeCatᵒᵖ} (f : X ⟶ Y),
  (Condensed.finYoneda F).map f = TypeCat.ofHom fun g => g ∘ ⇑(CategoryTheory.ConcreteCategory.hom f.unop)
-- Mathlib.Algebra.Group.Action.Faithful
/-- Two elements `m₁` and `m₂` are equal whenever they act in the same way on all points.  -/
FaithfulSMul.eq_of_smul_eq_smul : ∀ {M : Type u_4} {α : Type u_5} {inst : SMul M α} [self : FaithfulSMul M α] {m₁ m₂ : M},
  (∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_pow_sub_pow_sub : ∀ {E' : Type u_6} [inst : SeminormedAddCommGroup E'] (x₀ : E') {n m : ℕ},
  n < m → (fun x => ‖x - x₀‖ ^ m) =o[nhds x₀] fun x => ‖x - x₀‖ ^ n
-- Mathlib.AlgebraicTopology.CechNerve
/-- The morphism between Čech conerves associated to a morphism of arrows.  -/
CategoryTheory.Arrow.mapCechConerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
        [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] →
          (f ⟶ g) → (f.cechConerve ⟶ g.cechConerve)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- The points of the underlying topological space of `X ×[S] Y` bijectively correspond to
pairs of triples `x : X`, `y : Y`, `s : S` with `f x = s = f y` and prime ideals of
`κ(x) ⊗[κ(s)] κ(y)`.
 -/
AlgebraicGeometry.Scheme.Pullback.carrierEquiv : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} →
      ↥(CategoryTheory.Limits.pullback f g) ≃
        (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) × ↥(AlgebraicGeometry.Spec T.tensor)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_one : ∀ {α : Type u_2} [inst : One α] {a : α}, a ∈ 1 ↔ a = 1
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instSubmonoidClass : ∀ (M : Type u_1) [inst : MulOneClass M], SubmonoidClass (SaturatedSubmonoid M) M
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.apply : Aesop.RuleTerm → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
-- Init.Data.Array.Erase
Array.getElem?_eraseIdx : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {j : ℕ},
  (xs.eraseIdx i h)[j]? = if j < i then xs[j]? else xs[j + 1]?
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_finsupp_sum : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] {p : α → Prop} [inst_1 : Zero N]
  {s : β →₀ N} {h : β → N → α →₀ M},
  Finsupp.subtypeDomain p (s.sum h) = s.sum fun c d => Finsupp.subtypeDomain p (h c d)
-- Mathlib.Algebra.Order.Group.Synonym
isRightRegular_ofColex : ∀ {α : Type u_1} [inst : Monoid α] {a : Colex α}, IsRightRegular (ofColex a) ↔ IsRightRegular a
-- Mathlib.Algebra.Group.Submonoid.Defs
OneMemClass.coe_eq_one : ∀ {A : Type u_3} {M₁ : Type u_4} [inst : SetLike A M₁] [inst_1 : One M₁] [hA : OneMemClass A M₁] {S' : A} {x : ↥S'},
  ↑x = 1 ↔ x = 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).minKey? = some (t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k')
-- Init.Data.BitVec.Lemmas
BitVec.neg_eq_intMin : ∀ {w : ℕ} {x : BitVec w}, -x = BitVec.intMin w ↔ x = BitVec.intMin w
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Subring.integralClosure_le_iff : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {T : Subring A}
  [IsIntegrallyClosedIn (↥T) A], (integralClosure R A).toSubring ≤ T ↔ ∀ (r : R), (algebraMap R A) r ∈ T
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.image_closedBall : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ), ⇑e '' Metric.closedBall x r = Metric.closedBall (e x) r