mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the right half-plane. Let `f g : ℂ → E` be functions such
that

* `f` and `g` are differentiable in the open right half-plane and are continuous on its closure;
* `‖f z‖` and `‖g z‖` are bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open right
  half-plane for some `c < 2`;
* `‖f z‖` and `‖g z‖` are bounded from above by constants on the imaginary axis;
* `f x - g x`, `x : ℝ`, tends to zero superexponentially fast as `x → ∞`:
  for any natural `n`, `exp (n * x) * ‖f x - g x‖` tends to zero as `x → ∞`.

Then `f` is equal to `g` on the closed right half-plane.  -/
PhragmenLindelof.eqOn_right_half_plane_of_superexponential_decay : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E},
  DiffContOnCl ℂ f {z | 0 < z.re} →
    DiffContOnCl ℂ g {z | 0 < z.re} →
      (∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => Real.exp (B * ‖z‖ ^ c)) →
        (∃ c < 2, ∃ B, g =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => Real.exp (B * ‖z‖ ^ c)) →
          (Asymptotics.SuperpolynomialDecay Filter.atTop Real.exp fun x => ‖f ↑x - g ↑x‖) →
            (∃ C, ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) →
              (∃ C, ∀ (x : ℝ), ‖g (↑x * Complex.I)‖ ≤ C) → Set.EqOn f g {z | 0 ≤ z.re}
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_filter_of_pairwise_eq_one : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {f : κ → ι} {g : ι → M}
  {n : κ} {I : Finset κ},
  n ∈ I → ((↑I).Pairwise fun i j => f i = f j → g (f i) = 1) → ∏ j ∈ I with f j = f n, g (f j) = g (f n)
-- Std.Time.Date.PlainDate
/-- Creates a new `PlainDate` by adjusting the month to the given `month` value.
The day remains unchanged, and any invalid days for the new month will be handled according to the `clip` behavior.
 -/
Std.Time.PlainDate.withMonthClip : Std.Time.PlainDate → Std.Time.Month.Ordinal → Std.Time.PlainDate
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMapLinear_apply : ∀ (R : Type u) (M : Type v) (M₂ : Type w) (M₃ : Type y) (M₄ : Type z) (S : Type u_3) [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [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₃] [inst_9 : Module R M₄]
  [inst_10 : Module S M₃] [inst_11 : Module S M₄] [inst_12 : SMulCommClass R S M₃] [inst_13 : SMulCommClass R S M₄]
  (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₄)), (LinearMap.prodMapLinear R M M₂ M₃ M₄ S) f = f.1.prodMap f.2
-- Mathlib.Control.Functor.Multivariate
/-- `map` preserves compositions  -/
LawfulMvFunctor.comp_map : ∀ {n : ℕ} {F : TypeVec.{u_2} n → Type u_1} {inst : MvFunctor F} [self : LawfulMvFunctor F] {α β γ : TypeVec.{u_2} n}
  (g : α.Arrow β) (h : β.Arrow γ) (x : F α), MvFunctor.map (TypeVec.comp h g) x = MvFunctor.map h (MvFunctor.map g x)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_adj : ∀ {M : Type u_1} (s : Set M) [inst : Group M] (u v : M),
  (SimpleGraph.mulCayley s).Adj u v ↔ u ≠ v ∧ (u⁻¹ * v ∈ s ∨ v⁻¹ * u ∈ s)
-- Mathlib.AlgebraicTopology.SingularHomology.HomologyZero
TopCat.singularHomology₀Iso_sigma_desc_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.CategoryWithHomology C] (X : TopCat) (R : C),
  CategoryTheory.CategoryStruct.comp (X.singularHomology₀Iso R).hom
      (CategoryTheory.Limits.Sigma.desc fun x => CategoryTheory.CategoryStruct.id R) =
    X.singularHomology₀ε R
-- Mathlib.Analysis.Calculus.FDeriv.Pow
hasStrictFDerivAt_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  (n : ℕ) {x : 𝔸},
  HasStrictFDerivAt (fun x => x ^ n)
    (∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸) x
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.eq_or_eq_or_eq : ∀ {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β},
  G.Inc e x → G.Inc e y → G.Inc e z → x = y ∨ x = z ∨ y = z
-- Mathlib.Order.Filter.Prod
Filter.Tendsto.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} {m₁ : α → β} {m₂ : α → γ},
  Filter.Tendsto m₁ f g → Filter.Tendsto m₂ f h → Filter.Tendsto (fun x => (m₁ x, m₂ x)) f (g ×ˢ h)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstArrayRef.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that the intersection according to `Rci.HasRcoIntersection`
of two ranges contains exactly those elements that are contained in both ranges.
 -/
Std.Rci.LawfulRcoIntersection : (α : Type w) → [LT α] → [LE α] → [Std.Rci.HasRcoIntersection α] → Prop
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
UniqueFactorizationMonoid.moebius.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a : α),
  UniqueFactorizationMonoid.moebius a = if Squarefree a then (-1) ^ (UniqueFactorizationMonoid.factors a).card else 0
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.isColimitCocone`.

---

Any object `J : CardinalDirectedPoset κ` is a colimit
of its subsets that are of cardinality `< κ` and have a terminal object.  -/
CategoryTheory.CardinalFilteredPoset.isColimitCocone : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] → (J : CategoryTheory.CardinalDirectedPoset κ) → CategoryTheory.Limits.IsColimit J.cocone
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.instCoeOutLinearEquivId : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] →
            [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃ₗ[R] A₂)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.map_comp_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') {i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'')
  (f₃'' : k'' ⟶ l'')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃' ⟶ CategoryTheory.ComposableArrows.mk₃ f₁'' f₂'' f₃'')
  (n₀ n₁ n₂ : ℤ) (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.map_comp._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_comp._auto_3) {Z : C}
  (h : X.E f₁'' f₂'' f₃'' n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.map f₁ f₂ f₃ f₁'' f₂'' f₃'' (CategoryTheory.CategoryStruct.comp α β) n₀ n₁ n₂ hn₁ hn₂) h =
    CategoryTheory.CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.map f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂) h)
-- Mathlib.Order.RelSeries
LTSeries.mk_length : ∀ {α : Type u_1} [inst : Preorder α] (length : ℕ) (toFun : Fin (length + 1) → α) (strictMono : StrictMono toFun),
  (LTSeries.mk length toFun strictMono).length = length
-- Init.Data.Float.Float32
/-- Converts a 64-bit floating-point number to a 32-bit floating-point number.
This may lose precision.

This function does not reduce in the kernel.
 -/
Float.toFloat32 : Float → Float32
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) binary coproducts
preserves binary biproducts.  -/
CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F],
  CategoryTheory.Limits.PreservesBinaryBiproducts F
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- If `F` is a field, `A` is an `F`-algebra with fraction field `K`, `L` is a field,
`g : A →ₐ[F] L` lifts to `f : K →ₐ[F] L`,
`s` is a set such that the image of `g` is the subalgebra generated by `s`,
then the image of `f` is the intermediate field generated by `s`.
Note: this does not require `IsScalarTower F A K`.  -/
IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq : ∀ {F : Type u_1} {A : Type u_2} {K : Type u_3} {L : Type u_4} [inst : Field F] [inst_1 : CommRing A]
  [inst_2 : Algebra F A] [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra A K] [IsFractionRing A K]
  [inst_7 : Field L] [inst_8 : Algebra F L] {g : A →ₐ[F] L} {f : K →ₐ[F] L},
  (↑f).comp (algebraMap A K) = ↑g →
    ∀ {s : Set L}, g.range = Algebra.adjoin F s → f.fieldRange = IntermediateField.adjoin F s
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.continuous : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c), Continuous ↑f
-- Mathlib.Logic.Equiv.Defs
Equiv.nonempty_congr : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Nonempty α ↔ Nonempty β
-- Std.Time.Date.Unit.Day
Std.Time.Day.instDecidableLeOffset : {x y : Std.Time.Day.Offset} → Decidable (x ≤ y)
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The trivial submonoid `{1}` of a monoid `M`.  -/
Submonoid.instBot : {M : Type u_1} → [inst : MulOneClass M] → Bot (Submonoid M)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_iSup : ∀ {ι : Sort u_1} {G : Type u_2} [inst : Group G] (S : ι → Subgroup G), (iSup S).op = ⨆ i, (S i).op
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
act_rel_of_act_rel_of_rel_act_rel : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [ContravariantClass M N μ r] [IsTrans N r] (m : M)
  {a b c : N}, r (μ m a) b → r (μ m b) (μ m c) → r (μ m a) c
-- Mathlib.Algebra.Group.Action.Basic
smul_div' : ∀ {M : Type u_2} {A : Type u_3} [inst : Monoid M] [inst_1 : Group A] [inst_2 : MulDistribMulAction M A] (r : M)
  (x y : A), r • (x / y) = r • x / r • y
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.prod_mono_left : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (t : NonUnitalSubsemiring S), Monotone fun s => s.prod t
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a Dedekind domain,
the integral closure `C` of `A` in `L` is a Dedekind domain.

This cannot be an instance since `A`, `K` or `L` can't be inferred. See also the instance
`integralClosure.isDedekindDomain_fractionRing` where `K := FractionRing A`
and `C := integralClosure A L`.  -/
IsIntegralClosure.isDedekindDomain : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C] [IsScalarTower A C L]
  [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [IsDomain C] [IsDedekindDomain A], IsDedekindDomain C
-- Lean.DocString.Syntax
/-- Argument values  -/
Lean.Parser.Category.arg_val : Lean.Parser.Category
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- A group is commutative if the quotient by the center is cyclic.  -/
addCommGroupOfAddCyclicCenterQuotient : {G : Type u_2} →
  {G' : Type u_3} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup G'] → [IsAddCyclic G'] → (f : G →+ G') → f.ker ≤ AddSubgroup.center G → AddCommGroup G
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X},
  s.Nonempty → 1 ≤ (MeasureTheory.Measure.hausdorffMeasure 0) s
-- Mathlib.Analysis.Complex.HasPrimitives
/-- **Morera's theorem for the complex plane** A holomorphic function on `ℂ` has
primitives.
 -/
Differentiable.isExactOn_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E],
  Differentiable ℂ f → Complex.IsExactOn f Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.lift_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (hP : CategoryTheory.IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (hP.lift h k w) (CategoryTheory.CategoryStruct.comp snd h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Algebra.Category.ModuleCat.Injective
Module.injective_iff_injective_object : ∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Injective R M ↔ CategoryTheory.Injective (ModuleCat.of R M)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMonoidMorphism.mk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {H' : Type u_5} →
                [inst_4 : TopologicalSpace H'] →
                  {E' : Type u_6} →
                    [inst_5 : NormedAddCommGroup E'] →
                      [inst_6 : NormedSpace 𝕜 E'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {n : WithTop ℕ∞} →
                              {G : Type u_8} →
                                [inst_7 : TopologicalSpace G] →
                                  [inst_8 : ChartedSpace H G] →
                                    [inst_9 : Monoid G] →
                                      {G' : Type u_9} →
                                        [inst_10 : TopologicalSpace G'] →
                                          [inst_11 : ChartedSpace H' G'] →
                                            [inst_12 : Monoid G'] →
                                              (toMonoidHom : G →* G') →
                                                ContMDiff I I' n (↑toMonoidHom).toFun →
                                                  ContMDiffMonoidMorphism I I' n G G'
-- Mathlib.Analysis.Normed.Ring.Basic
norm_mul₃_le : ∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] {a b c : α}, ‖a * b * c‖ ≤ ‖a‖ * ‖b‖ * ‖c‖
-- Init.Data.Nat.Simproc
Nat.Simproc.add_eq_add_ge : ∀ (a c : ℕ) {b d : ℕ}, b ≥ d → (a + b = c + d) = (a + (b - d) = c)
-- Mathlib.Order.Filter.Pointwise
Filter.instInvolutiveNeg.eq_1 : ∀ {α : Type u_2} [inst : InvolutiveNeg α], Filter.instInvolutiveNeg = { toNeg := Filter.instNeg, neg_neg := ⋯ }
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- Every expression $\sum_i m_i \otimes n_i$ which vanishes also vanishes trivially if and only if
for every submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is injective.  -/
TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N],
  (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔
    ∀ (M' : Submodule R M), Function.Injective ⇑(LinearMap.rTensor N M'.subtype)
-- Mathlib.Combinatorics.Graph.Subgraph
/-- `H ≤ G` means `H` is a subgraph of `G`. It is defined as `V(H) ⊆ V(G)` and every link of `H`
being a link of `G`.  -/
Graph.instPartialOrder : {α : Type u_1} → {β : Type u_2} → PartialOrder (Graph α β)
-- Init.Data.Int.Gcd
Int.gcd_sub_self_right : ∀ (m n : ℤ), m.gcd (n - m) = m.gcd n
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableInf₂.measurable_inf : ∀ {M : Type u_1} {inst : MeasurableSpace M} {inst_1 : Min M} [self : MeasurableInf₂ M], Measurable fun p => p.1 ⊓ p.2
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits, then `F.unop : C ⥤ D` reflects limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [inst_3 : NeZero i] (hi : Even i)
  (x y : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) x =
      (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Rep.Hom.hom A.norm).range
-- Mathlib.Data.Set.Function
Set.BijOn.symm : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {g : β → α},
  Set.InvOn f g t s → Set.BijOn f s t → Set.BijOn g t s
-- Mathlib.Logic.Function.Basic
Function.extend_def : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (e' : β → γ) (b : β)
  [inst : Decidable (∃ a, f a = b)],
  Function.extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b
-- Mathlib.Condensed.Discrete.Colimit
Condensed.locallyConstantIsoFinYoneda.eq_1 : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))),
  Condensed.locallyConstantIsoFinYoneda F =
    CategoryTheory.NatIso.ofComponents
      (fun Y =>
        { hom := TypeCat.ofHom fun f => f.toFun, inv := TypeCat.ofHom fun f => { toFun := f, isLocallyConstant := ⋯ },
          hom_inv_id := ⋯, inv_hom_id := ⋯ })
      ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.Plus.instRespectsIsoQuasiIso : ∀ (A : Type u_3) [inst : CategoryTheory.Category.{v_3, u_3} A] [inst_1 : CategoryTheory.Abelian A],
  (HomotopyCategory.Plus.quasiIso A).RespectsIso
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.k_mul_i : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), q.k * q.i = -c₁ • q.j
-- Mathlib.Data.Nat.Fib.Zeckendorf
instIsTransNatLeHAddOfNat : IsTrans ℕ fun a b => b + 2 ≤ a
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_map : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {G : Type u_7} [inst_4 : NormedAddCommGroup G]
  [inst_5 : InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G), ⇑(b.map L) = ⇑L ∘ ⇑b
-- Lean.Data.Options
Lean.MonadOptions.mk : {m : Type → Type} → m Lean.Options → Lean.MonadOptions m
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.IsAffineMap.mk : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] [inst_4 : Convexity.ConvexSpace R N]
  {f : M → N},
  (∀ (s : Convexity.StdSimplex R M),
      f (Convexity.sConvexComb s) = Convexity.sConvexComb (Convexity.StdSimplex.map f s)) →
    Convexity.IsAffineMap R f
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.algebra : {𝕜 : Type u_1} →
  {I : Type u_5} →
    {B : I → Type u_6} →
      [inst : NormedField 𝕜] →
        [inst_1 : (i : I) → NormedRing (B i)] → [(i : I) → NormedAlgebra 𝕜 (B i)] → Algebra 𝕜 (PreLp B)
-- Mathlib.RingTheory.SimpleModule.Isotypic
LinearEquiv.isotypicComponent_eq : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup S] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R S]
  (e : N ≃ₗ[R] S), isotypicComponent R M N = isotypicComponent R M S
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Scalar multiplication distributes across addition  -/
DistribMulAction.smul_add : ∀ {M : Type u_12} {A : Type u_13} {inst : Monoid M} {inst_1 : AddMonoid A} [self : DistribMulAction M A] (a : M)
  (x y : A), a • (x + y) = a • x + a • y
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_dropn : ∀ {α : Type u} (s : Stream'.WSeq α) (n : ℕ), (s.drop n).destruct = s.destruct >>= Stream'.WSeq.drop.aux n
-- Mathlib.Order.Filter.Prod
Filter.prod_sup : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g₁ g₂ : Filter β), f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- A natural isomorphism between the functors `toOver Y` and `toOver X ⋙ pullback f`
for any morphism `f : X ⟶ Y`.  -/
CategoryTheory.toOverPullbackIsoToOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {X Y : C} →
        (f : Y ⟶ X) →
          [inst_2 : CategoryTheory.ChosenPullbacksAlong f] →
            (CategoryTheory.toOver X).comp (CategoryTheory.ChosenPullbacksAlong.pullback f) ≅ CategoryTheory.toOver Y
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- The induction hypothesis of `Submodule.basisOfPid` and `Submodule.smithNormalForm`.

Basically, it says: let `N ≤ M` be a pair of submodules, then we can find a pair of
submodules `N' ≤ M'` of strictly smaller rank, whose basis we can extend to get a basis
of `N` and `M`. Moreover, if the basis for `M'` is up to scalars a basis for `N'`,
then the basis we find for `M` is up to scalars a basis for `N`.

For `basis_of_pid` we only need the first half and can fix `M = ⊤`,
for `smith_normal_form` we need the full statement,
but must also feed in a basis for `M` using `basis_of_pid` to keep the induction going.
 -/
Submodule.basis_of_pid_aux : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [IsPrincipalIdealRing R] [IsDomain R] [Finite ι] {O : Type u_4}
  [inst_4 : AddCommGroup O] [inst_5 : Module R O] (M N : Submodule R O) (b'M : Module.Basis ι R ↥M),
  N ≠ ⊥ →
    N ≤ M →
      ∃ y ∈ M,
        ∃ a,
          a • y ∈ N ∧
            ∃ M' ≤ M,
              ∃ N' ≤ N,
                N' ≤ M' ∧
                  (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                    (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                      ∀ (n' : ℕ) (bN' : Module.Basis (Fin n') R ↥N'),
                        ∃ bN,
                          ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Module.Basis (Fin m') R ↥M'),
                            ∃ (hnm : n' + 1 ≤ m' + 1),
                              ∃ bM,
                                ∀ (as : Fin n' → R),
                                  (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                    ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
-- Batteries.Data.Array.Scan
Array.take_scanl : ∀ {β : Type u_1} {α : Type u_2} {i : ℕ} {f : β → α → β} (init : β) (as : Array α),
  (Array.scanl f init as).take (i + 1) = Array.scanl f init (as.take i)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.isLUB_sSup' : ∀ {β : Type u_5} [inst : ConditionallyCompleteLattice β] {s : Set (WithBot β)}, BddAbove s → IsLUB s (sSup s)