mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
/-- Euclid's lemma: if `a ∣ b * c` and `a` and `b` have no common prime factors, `a ∣ c`.
Compare `IsCoprime.dvd_of_dvd_mul_right`.  -/
UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b c : R},
  a ≠ 0 → (∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d) → a ∣ b * c → a ∣ c
-- Init.Data.Int.Cooper
_private.Init.Data.Int.Cooper.0.Int.add_of_le.eq_1 : ∀ {a b : ℤ} (h : a ≤ b), Int.add_of_le h = ⟨(b - a).toNat, ⋯⟩
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_replaceₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ (a : α) (b : β a), Std.DHashMap.Internal.Raw.WFImp ↑(m.replaceₘ a b)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.mulActionHom_compl.congr_simp : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α]
  [inst_3 : Fintype α] {m : ℕ} (hm : m + n = Fintype.card α),
  Set.powersetCard.mulActionHom_compl G α hm = Set.powersetCard.mulActionHom_compl G α hm
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Scheme.Hom.cover_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (hf : P f)
  [inst : AlgebraicGeometry.Surjective f], (AlgebraicGeometry.Scheme.Hom.cover f hf).I₀ = PUnit.{v + 1}
-- Aesop.Rule.Name
Aesop.RuleName.hash : Aesop.RuleName → UInt64
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.idxAuxOf_toArray : ∀ {α : Type u_1} {l' : List α} [inst : BEq α] (a : α) (l : List α) (j : ℕ),
  l' = List.drop j l →
    ∀ (h : l'.length + j = l.length), l.toArray.idxOfAux a j = List.findFinIdx?.go (fun x => x == a) l l' j h
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_submatrix : ∀ {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype n₀]
  [inst_2 : CommSemiring R] (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n), (A.submatrix ⇑em ⇑en).rank = A.rank
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult.mk.inj : ∀ {uvars : Array Lean.Elab.Term.Do.Var} {term : Lean.Syntax} {uvars_1 : Array Lean.Elab.Term.Do.Var}
  {term_1 : Lean.Syntax},
  { uvars := uvars, term := term } = { uvars := uvars_1, term := term_1 } → uvars = uvars_1 ∧ term = term_1
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- A subtype-like structure for full subcategories. Morphisms just ignore the property. We don't use
actual subtypes since the simp-normal form `↑X` of `X.val` does not work well for full
subcategories.  -/
CategoryTheory.ObjectProperty.FullSubcategory : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Type u
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet.mk.injEq : ∀ (parents parents_1 : List Lean.Expr), ({ parents := parents } = { parents := parents_1 }) = (parents = parents_1)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.pullback_refine : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD] {Y X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} {S T : J.Cover X} (h : S ⟶ T) (f : Y ⟶ X) (x : CategoryTheory.Meq P T),
  (x.pullback f).refine ((J.pullback f).map h) = (x.refine h).pullback f
-- Mathlib.MeasureTheory.Measure.Complex
/-- The complex measures form a linear isomorphism to the type of pairs of signed measures.  -/
MeasureTheory.ComplexMeasure.equivSignedMeasureₗ : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {R : Type u_2} →
      [inst : Semiring R] →
        [inst_1 : Module R ℝ] →
          [inst_2 : ContinuousConstSMul R ℝ] →
            [inst_3 : ContinuousConstSMul R ℂ] →
              MeasureTheory.ComplexMeasure α ≃ₗ[R] MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function and `x : R` is
multiplicative for `f`, then `x` is multiplicative for `seminormFromBounded' f`.  -/
seminormFromBounded_of_mul_is_mul : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f →
    (∀ (x y : R), f (x * y) ≤ c * f x * f y) →
      ∀ {x : R},
        (∀ (y : R), f (x * y) = f x * f y) →
          ∀ (y : R), seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y
-- Mathlib.Topology.Algebra.UniformConvergence
instDistribMulActionUniformOnFun : {α : Type u_1} →
  {β : Type u_2} →
    {𝔖 : Set (Set α)} →
      {M : Type u_5} →
        [inst : Monoid M] → [inst_1 : AddMonoid β] → [DistribMulAction M β] → DistribMulAction M (UniformOnFun α β 𝔖)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {l : List ((a : α) × β a)},
  Std.DHashMap.ofList l = ∅.insertMany l
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  ⦃i : ι⦄ {Z : C} (q : Z ⟶ X i) ⦃j : ι'⦄ (a : Z ⟶ X' j)
  (fac : CategoryTheory.CategoryStruct.comp a (f' j) = CategoryTheory.CategoryStruct.comp q (f i)) {Z' : C} (r : Z' ⟶ Z)
  (r' : Z' ⟶ X i) (a' : Z' ⟶ X' j)
  (hr' :
    autoParam (CategoryTheory.CategoryStruct.comp r q = r')
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_precomp._auto_1✝)
  (ha' :
    autoParam (CategoryTheory.CategoryStruct.comp r a = a')
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_precomp._auto_3✝),
  CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ r' a' ⋯ =
    (CategoryTheory.ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (CategoryTheory.Over.homMk r ⋯).op))
      (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ q a fac)
-- Mathlib.Topology.Order.LeftRight
continuousAt_iff_continuous_left_right : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace β]
  {a : α} {f : α → β}, ContinuousAt f a ↔ ContinuousWithinAt f (Set.Iic a) a ∧ ContinuousWithinAt f (Set.Ici a) a
-- Mathlib.Analysis.Complex.LocallyUniformLimit
Complex.cderiv_eq_deriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U : Set ℂ} {z : ℂ} {r : ℝ} {f : ℂ → E}
  [CompleteSpace E],
  IsOpen U → DifferentiableOn ℂ f U → 0 < r → Metric.closedBall z r ⊆ U → Complex.cderiv r f z = deriv f z
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.image_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M M' M'' : CategoryTheory.Functor C MonCat}
  (S : CategoryTheory.SubmonoidFunctor M) (p : M ⟶ M') (p' : M' ⟶ M''),
  CategoryTheory.SubmonoidFunctor.image (CategoryTheory.CategoryStruct.comp p p') S =
    CategoryTheory.SubmonoidFunctor.image p' (CategoryTheory.SubmonoidFunctor.image p S)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap.0.WeierstrassCurve.CXX : ∀ {R : Type u_1} [inst : CommRing R] {i : Fin 3} {a : R}, (MvPolynomial.C a * MvPolynomial.X i ^ 2).IsHomogeneous 2
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_zsmul_sub_self : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp a b • p - b = -toIcoMod hp a b
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.coe_toSubmonoid_symm_apply : ∀ {A : Type u_4} [inst : AddZeroClass A] (S : Submonoid (Multiplicative A)),
  ↑((RelIso.symm AddSubmonoid.toSubmonoid) S) = ⇑Multiplicative.ofAdd ⁻¹' ↑S
-- Mathlib.RingTheory.Extension.Generators
/-- If `R → S → T` is a tower of algebras, a family of generators `R[X] → T`
gives a family of generators `S[X] → T`.  -/
Algebra.Generators.extendScalars : {R : Type u} →
  (S : Type v) →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {T : Type u_2} →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] →
                  [inst_5 : Algebra S T] → [IsScalarTower R S T] → Algebra.Generators R T ι → Algebra.Generators S T ι
-- Lean.Parser.Do
Lean.Parser.Term.doContinue.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mkHom_surjective : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M}, Function.Surjective ⇑AddLocalization.mkHom
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.iteration_map_succ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_4 :
    ∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  (κ : Cardinal.{w}) [inst_5 : OrderBot κ.ord.ToType]
  [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [inst_7 : Fact κ.IsRegular] (j : κ.ord.ToType)
  {Z_1 : C} (h : (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj (Order.succ j) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯)) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.OrthogonalReflection.toStep W ((CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.OrthogonalReflection.fromStep W ((CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.iterationObjSuccIso W Z κ j).inv h))
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_iff_image : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_6}
  {s : Set ι} {f : ι → M}, Set.InjOn f s → (LinearIndepOn R f s ↔ LinearIndepOn R id (f '' s))
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.cancel_natIso_hom_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) {X : C} {Y : D} (g g' : G.obj X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (α.hom.app X) g = CategoryTheory.CategoryStruct.comp (α.hom.app X) g' ↔ g = g'
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.disjoint_fromEdgeSet : ∀ {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)), Disjoint G (SimpleGraph.fromEdgeSet s) ↔ Disjoint G.edgeSet s
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_mul_single : ∀ {Γ' : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : PartialOrder Γ']
  [inst_2 : AddCommGroup Γ'] [inst_3 : IsOrderedAddMonoid Γ'] {r : R} {x : HahnSeries Γ' R} {a b : Γ'},
  (x * (HahnSeries.single b) r).coeff a = x.coeff (a - b) * r
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.position : Lean.Elab.InlayHintInfo → String.Pos.Raw
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.erase.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) l.size → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) l.size) →
          ((l' : Std.DTreeMap.Internal.Impl α β) →
              (hl'₁ : l'.Balanced) →
                (hl'₂ : l.size - 1 ≤ l'.size) →
                  (hl'₃ : l'.size ≤ l.size) →
                    motive { impl := l', balanced_impl := hl'₁, lb_le_size_impl := hl'₂, size_impl_le_ub := hl'₃ }) →
            motive x
-- Mathlib.GroupTheory.Complement
Subgroup.instInhabitedLeftTransversal : {G : Type u_1} → [inst : Group G] → {H : Subgroup G} → Inhabited H.LeftTransversal
-- Mathlib.CategoryTheory.Comma.Final
CategoryTheory.Comma.final_fst_of_isConnected_structuredArrow : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [∀ (a : A), CategoryTheory.IsConnected (CategoryTheory.StructuredArrow (L.obj a) R)],
  (CategoryTheory.Comma.fst L R).Final
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α), G.diam = G.ediam.toNat
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
quadraticCharFun.eq_1 : ∀ (α : Type u_1) [inst : MonoidWithZero α] [inst_1 : DecidableEq α] [inst_2 : DecidablePred IsSquare] (a : α),
  quadraticCharFun α a = if a = 0 then 0 else if IsSquare a then 1 else -1
-- Mathlib.RingTheory.Flat.Basic
/-- If `M`, `N` are `R`-modules, there exists an injective `R`-linear map from `R` to `M`,
and `N` is a nontrivial flat `R`-module, then `M ⊗[R] N` is nontrivial.  -/
TensorProduct.nontrivial_of_linearMap_injective_of_flat_right : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) (N : Type u_3) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : R →ₗ[R] M),
  Function.Injective ⇑f → ∀ [Module.Flat R N] [Nontrivial N], Nontrivial (TensorProduct R M N)
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.inv_cpow_ofReal_nonneg : ∀ {a : ℝ}, 0 ≤ a → ∀ (r : ℂ), (↑a)⁻¹ ^ r = (↑a ^ r)⁻¹
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.mem_range_of_isRoot : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : CommRing S] [IsDomain S] {f : Polynomial R},
  f.Splits → f ≠ 0 → ∀ {i : R →+* S} {x : S}, (Polynomial.map i f).IsRoot x → x ∈ i.range
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeasToLpTrim_ae_eq : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  (f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)), ↑↑(MeasureTheory.lpMeasToLpTrim F 𝕜 p μ hm f) =ᵐ[μ] ↑↑↑f
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_subset`. -/
Set.setOf_subset : ∀ {α : Type u} {p : α → Prop} {s : Set α}, Set.ofPred p ⊆ s ↔ ∀ (x : α), p x → x ∈ s
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piSplitLE.eq_1 : ∀ {ι : Type u_6} {X : ι → Type u_8} {i : ι} [inst : PartialOrder ι] [inst_1 : DecidableEq ι],
  InverseSystem.piSplitLE =
    { toFun := fun f j => if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩,
      invFun := fun f => (fun j => f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `lowerHemicontinuousWithinAt_singleton_iff`. -/
ContinuousWithinAt.lowerHemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → LowerHemicontinuousWithinAt (fun x => {f x}) s x
-- Mathlib.LinearAlgebra.Ray
/-- Scaling by an inverse unit is the same as scaling by itself.  -/
units_inv_smul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (u : Rˣ) (v : Module.Ray R M), u⁻¹ • v = u • v
-- Init.Data.Vector.Lemmas
Vector.mem_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {b : β} {f : α → β} {xs : Vector α n}, b ∈ Vector.map f xs ↔ ∃ a ∈ xs, f a = b
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_replicate : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.Refl fun x1 x2 => x1 ≤ x2] {n : ℕ} {a : α}
  {f : α → β} (h : List.replicate n a ≠ []), List.maxIdxOn f (List.replicate n a) h = 0
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.map_jacobson_of_surjective : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] {I : Ideal R} {f : R →+* S},
  Function.Surjective ⇑f → RingHom.ker f ≤ I → Ideal.map f I.jacobson = (Ideal.map f I).jacobson
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.closedBall_zero_eq_Icc' : ∀ (c : NNReal), Metric.closedBall 0 ↑c = Set.Icc 0 c
-- Mathlib.Algebra.Group.Action.Option
Option.smul_none : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] (a : M), a • none = none
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_finsetSum_vectorMeasure : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] (μ : ι → MeasureTheory.VectorMeasure X F)
  (B : E →L[ℝ] F →L[ℝ] G) (s : Finset ι), (∑ i ∈ s, μ i).transpose B = ∑ i ∈ s, (μ i).transpose B
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedCommRing α] [NormMulClass α] [NormOneClass α] (s : Finset β)
  (f : β → α), ‖∏ b ∈ s, f b‖₊ = ∏ b ∈ s, ‖f b‖₊
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.step_uLift.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.inv_comp_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.GrpObj A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv
      (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h) =
    h
-- Mathlib.NumberTheory.Real.Irrational
irrational_intCast_mul_iff : ∀ {m : ℤ} {x : ℝ}, Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x
-- Mathlib.Algebra.Category.ModuleCat.Semi
linearEquivIsoModuleIsoₛ_hom : ∀ {R : Type u} [inst : Semiring R] {X Y : Type u} [inst_1 : AddCommMonoid X] [inst_2 : AddCommMonoid Y]
  [inst_3 : Module R X] [inst_4 : Module R Y], linearEquivIsoModuleIsoₛ.hom = TypeCat.ofHom fun e => e.toModuleIsoₛ
-- Init.Data.Vector.Lemmas
Vector.prod_eq_foldr : ∀ {α : Type u_1} {n : ℕ} [inst : Mul α] [inst_1 : One α] {xs : Vector α n},
  xs.prod = Vector.foldr (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
add_le_of_le_tsub_right_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, b ≤ c → a ≤ c - b → a + b ≤ c
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.SolveByElimConfig.mk : Lean.Meta.SolveByElim.ApplyRulesConfig → Bool → Bool → Bool → Bool → Lean.Meta.SolveByElim.SolveByElimConfig
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [inst_4 : CategoryTheory.Limits.HasProduct X]
  [inst_5 : CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Fibration (f i)]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)]
  [∀ (i : J), HomotopicalAlgebra.WeakEquivalence (f i)],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.Pi.map f)
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.isPosSemidef_covarianceBilin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E}, (ProbabilityTheory.covarianceBilin μ).toBilinForm.IsPosSemidef
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- Introduce a function `inverse` on a monoid with zero `M₀`, which sends `x` to `x⁻¹` if `x` is
invertible and to `0` otherwise.  This definition is somewhat ad hoc, but one needs a fully (rather
than partially) defined inverse function for some purposes, including for calculus.

Note that while this is in the `Ring` namespace for brevity, it requires the weaker assumption
`MonoidWithZero M₀` instead of `Ring M₀`.  -/
Ring.inverse : {M₀ : Type u_2} → [MonoidWithZero M₀] → M₀ → M₀
-- Aesop.Stats.Extension
Aesop.recordStatsIfEnabled : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadOptions m] → Aesop.StatsExtensionEntry → m Unit
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
le_integralClosure_iff_isIntegral : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  S ≤ integralClosure R A ↔ Algebra.IsIntegral R ↥S
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.weakEquivalences_op_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.WeakEquivalence f.op ↔ HomotopicalAlgebra.WeakEquivalence f
-- Init.Data.Option.Array
Option.foldlM_toArray : ∀ {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option β) (a : α)
  (f : α → β → m α), Array.foldlM f a o.toArray = o.elim (pure a) fun b => f a b
-- Mathlib.Data.List.TFAE
/-- If `P₁ x ↔ ... ↔ Pₙ x` for all `x`, then `(∀ x, P₁ x) ↔ ... ↔ (∀ x, Pₙ x)`.
Note: in concrete cases, Lean has trouble finding the list `[P₁, ..., Pₙ]` from the list
`[(∀ x, P₁ x), ..., (∀ x, Pₙ x)]`, but simply providing a list of underscores with the right
length makes it happier.

Example:
```lean
example (P₁ P₂ P₃ : ℕ → Prop) (H : ∀ n, [P₁ n, P₂ n, P₃ n].TFAE) :
    [∀ n, P₁ n, ∀ n, P₂ n, ∀ n, P₃ n].TFAE :=
  forall_tfae [_, _, _] H
```
 -/
List.forall_tfae : ∀ {α : Type u_1} (l : List (α → Prop)),
  (∀ (a : α), (List.map (fun p => p a) l).TFAE) → (List.map (fun p => ∀ (a : α), p a) l).TFAE