mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.DFinsupp
/-- Given a family of linear maps `f i : M i →ₗ[R] N`, we can form a linear map
`(Π₀ i, M i) →ₗ[R] N` which sends `x : Π₀ i, M i` to the sum over `i` of `f i` applied to `x i`.
This is the map coming from the universal property of `Π₀ i, M i` as the coproduct of the `M i`.
See also `LinearMap.coprod` for the binary product version.  -/
DFinsupp.coprodMap : {ι : Type u_1} →
  {R : Type u_3} →
    {M : ι → Type u_5} →
      {N : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] → [DecidableEq ι] → ((i : ι) → M i →ₗ[R] N) → (Π₀ (i : ι), M i) →ₗ[R] N
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_alter_of_beq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF → (k == k') = true → (k' ∈ m.alter k f ↔ (f m[k]?).isSome = true)
-- Mathlib.Order.CompleteLattice.Basic
biSup_le_eq_sup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : PartialOrder ι] (f : ι → α) (i : ι),
  ⨆ j, ⨆ (_ : j ≤ i), f j = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.rendered : Aesop.RuleName.Json✝ → String
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.inj.sizeOf_spec : ∀ (origin : Lean.Meta.Grind.Origin), sizeOf (Lean.Meta.Grind.SplitSource.inj origin) = 1 + sizeOf origin
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.levelParams : Lean.Elab.Command.FinalizeContext✝ → List Lean.Name
-- Init.Data.List.Find
List.findIdx?_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool}, List.findIdx? p [a] = if p a = true then some 0 else none
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_pow' : ∀ {m : ℤ} {n : ℕ}, n ≠ 0 → (Odd (m ^ n) ↔ Odd m)
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : Monoid X] [inst_1 : Monoid Y] (f : X →* Y),
  MonCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.Algebra.Category.Grp.Zero
GrpCat.isZero_of_subsingleton : ∀ (G : GrpCat) [Subsingleton ↑G], CategoryTheory.Limits.IsZero G
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.SavedState.tactic : Lean.Elab.Tactic.SavedState → Lean.Elab.Tactic.State
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_div_cancel : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a : α}, IsUnit a → ∀ (b : α), a * (b / a) = b
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Inverse of an affine equivalence as an affine equivalence.  -/
AffineEquiv.symm : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → (P₁ ≃ᵃ[k] P₂) → P₂ ≃ᵃ[k] P₁
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_left_i : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).left.i =
    X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Ideal.finrank_fiber_eq_finrank : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] [IsDomain R] (p : Ideal R) [inst_6 : p.IsPrime],
  Module.finrank p.ResidueField (p.Fiber M) = Module.finrank R M
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_map_of_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F] [F.Faithful],
  CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i) → CategoryTheory.IsPullback f g h i
-- Mathlib.GroupTheory.OrderOfElement
/-- This is the same as `addOrderOf_nsmul'` and
`addOrderOf_nsmul` but with one assumption less which is automatic in the case of a
finite cancellative additive monoid.  -/
addOrderOf_nsmul : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] [Finite G] {n : ℕ} (x : G),
  addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n
-- Mathlib.Data.Nat.Factorial.Basic
/-- Factorial implemented using binary splitting.

While this still performs the same number of multiplications,
the big-integer operands to each are much smaller.  -/
Nat.factorialBinarySplitting : ℕ → ℕ
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq_disjoint : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  Pairwise (Function.onFun Disjoint (MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i))
-- Mathlib.Topology.Order.Hom.Esakia
/-- The type of pseudo-epimorphisms, aka p-morphisms, aka bounded maps, from `α` to `β`.  -/
PseudoEpimorphism : (α : Type u_6) → (β : Type u_7) → [Preorder α] → [Preorder β] → Type (max u_6 u_7)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instOne : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → One (FractionalIdeal S P)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mk.injEq : ∀ {α : Type u_6} [inst : LE α] (toProd : α × α) (fst_le_snd : toProd.1 ≤ toProd.2) (toProd_1 : α × α)
  (fst_le_snd_1 : toProd_1.1 ≤ toProd_1.2),
  ({ toProd := toProd, fst_le_snd := fst_le_snd } = { toProd := toProd_1, fst_le_snd := fst_le_snd_1 }) =
    (toProd = toProd_1)
-- Batteries.Data.List.Lemmas
List.findIdxs_eq_nil_iff : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ}, List.findIdxs p xs s = [] ↔ ∀ x ∈ xs, p x = false
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.foldM_eq_foldlM_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap α fun x => β} [inst : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  Std.DHashMap.foldM f init m = Array.foldlM (fun a b => f a b.1 b.2) init (Std.DHashMap.Const.toArray m)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_naturality_right : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.BraidedCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_ X Z).hom =
    CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF)
  (h' : k ∈ Std.DTreeMap.Raw.filterMap f t), (f k (t.get k ⋯)).isSome = true
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₁_append_right : ∀ (s t : List Char) (i b : ℕ) (e : String.Pos.Raw),
  b = String.utf8Len s + i →
    String.Pos.Raw.extract.go₁ (s ++ t) { byteIdx := i } { byteIdx := b } e =
      String.Pos.Raw.extract.go₂ t { byteIdx := b } e
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.map_fundamentalDomain : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace K F] (f : E ≃ₗ[K] F),
  ⇑f '' ZSpan.fundamentalDomain b = ZSpan.fundamentalDomain (b.map f)
-- Mathlib.Data.Finsupp.Defs
Finsupp.instSubsingleton : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [IsEmpty α], Subsingleton (α →₀ M)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Ici_iff_integrableOn_Ioi' : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {b : α},
  autoParam (μ {b} ≠ ⊤) integrableOn_Ici_iff_integrableOn_Ioi'._auto_1 →
    autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Ici_iff_integrableOn_Ioi'._auto_3 →
      (MeasureTheory.IntegrableOn f (Set.Ici b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioi b) μ)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFreeOn.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α) (s : Set α) (n : ℕ),
  G.CliqueFreeOn s n = ∀ ⦃t : Finset α⦄, ↑t ⊆ s → ¬G.IsNClique n t
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- A piecewise function on countably many pieces is measurable if all the data is measurable.  -/
Measurable.find : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {x : MeasurableSpace α} {f : ℕ → α → β} {p : ℕ → α → Prop}
  [inst : (n : ℕ) → DecidablePred (p n)],
  (∀ (n : ℕ), Measurable (f n)) →
    (∀ (n : ℕ), MeasurableSet {x | p n x}) → ∀ (h : ∀ (x : α), ∃ n, p n x), Measurable fun x => f (Nat.find ⋯) x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instMinOfT2Space : {α : Type u_1} → [inst : TopologicalSpace α] → [T2Space α] → Min (TopologicalSpace.Compacts α)
-- Mathlib.ModelTheory.Definability
Set.Definable.inter : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {f g : Set (α → M)},
  A.Definable L f → A.Definable L g → A.Definable L (f ∩ g)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtension_iff_precomp : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (F' : CategoryTheory.Functor D H) (G : CategoryTheory.Functor C' C) [G.IsEquivalence] (α : F ⟶ L.comp F'),
  F'.IsLeftKanExtension α ↔
    F'.IsLeftKanExtension (CategoryTheory.CategoryStruct.comp (G.whiskerLeft α) (G.associator L F').inv)
-- Mathlib.Data.Sign.Defs
instDecidableEqSignType : DecidableEq SignType
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_dvd_iff : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] {A : Matrix m n ℚ} {r : ℕ},
  A.den ∣ r ↔ ∀ (i : m) (j : n), (A i j).den ∣ r
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_polynomialY : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W.baseChange B).polynomialY = Polynomial.map (Polynomial.mapRingHom ↑f) (W.baseChange A).polynomialY
-- Mathlib.GroupTheory.OrderOfElement
finEquivPowers.eq_1 : ∀ {G : Type u_1} [inst : Monoid G] {x : G} (hx : IsOfFinOrder x),
  finEquivPowers hx = Equiv.ofBijective (fun n => ⟨x ^ ↑n, ⋯⟩) ⋯
-- Init.Core
/-- `Commutative op` says that `op` is a commutative operation,
i.e. `a ∘ b = b ∘ a`.
 -/
Std.Commutative : {α : Sort u} → (α → α → α) → Prop
-- Mathlib.Topology.Algebra.UniformRing
/-- The map from a uniform ring to its completion, as a ring homomorphism.  -/
UniformSpace.Completion.coeRingHom : {α : Type u_1} →
  [inst : Ring α] →
    [inst_1 : UniformSpace α] →
      [inst_2 : IsTopologicalRing α] → [inst_3 : IsUniformAddGroup α] → α →+* UniformSpace.Completion α
-- Mathlib.GroupTheory.MonoidLocalization.Divisibility
Submonoid.LocalizationMap.map_isUnit_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] {S : Submonoid M} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {m : M}, IsUnit (f m) ↔ ∃ s ∈ S, m ∣ s
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.inr_comp_pushoutObjIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (f.app d) (g.app d))
      (CategoryTheory.Limits.pushoutObjIso f g d).inv =
    (CategoryTheory.Limits.pushout.inr f g).app d
-- Mathlib.Combinatorics.Graph.Basic
Graph.mem_incidenceSet : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) (e : β), e ∈ Graph.incidenceSet x ↔ G.Inc e x
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.orthogonalProjectionOnto_apply_eq_projectionOnto : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (x : E),
  K.orthogonalProjectionOnto x = (K.projectionOnto Kᗮ ⋯) x
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.mk.inj : ∀ {ruleExprName : Lean.Name} {builderName : Aesop.BuilderName} {scopeName : Aesop.ScopeName} {tac : Aesop.RuleTacDescr}
  {indexingMode : Aesop.IndexingMode} {pattern? : Option Aesop.RulePattern} {ruleExprName_1 : Lean.Name}
  {builderName_1 : Aesop.BuilderName} {scopeName_1 : Aesop.ScopeName} {tac_1 : Aesop.RuleTacDescr}
  {indexingMode_1 : Aesop.IndexingMode} {pattern?_1 : Option Aesop.RulePattern},
  { ruleExprName := ruleExprName, builderName := builderName, scopeName := scopeName, tac := tac,
        indexingMode := indexingMode, pattern? := pattern? } =
      { ruleExprName := ruleExprName_1, builderName := builderName_1, scopeName := scopeName_1, tac := tac_1,
        indexingMode := indexingMode_1, pattern? := pattern?_1 } →
    ruleExprName = ruleExprName_1 ∧
      builderName = builderName_1 ∧
        scopeName = scopeName_1 ∧ tac = tac_1 ∧ indexingMode = indexingMode_1 ∧ pattern? = pattern?_1
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.cast : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} →
        {aig1 aig2 : Std.Sat.AIG α} → aig1.BinaryRefVec len → aig1.decls.size ≤ aig2.decls.size → aig2.BinaryRefVec len
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.mk.injEq : ∀ {α : Type u_2} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (indep_maximal : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (E_1 : Set α) (Indep_1 : Set α → Prop) (indep_empty_1 : Indep_1 ∅)
  (indep_subset_1 : ∀ ⦃I J : Set α⦄, Indep_1 J → I ⊆ J → Indep_1 I)
  (indep_aug_1 :
    ∀ ⦃I B : Set α⦄, Indep_1 I → ¬Maximal Indep_1 I → Maximal Indep_1 B → ∃ x ∈ B \ I, Indep_1 (insert x I))
  (indep_maximal_1 : ∀ X ⊆ E_1, Matroid.ExistsMaximalSubsetProperty Indep_1 X)
  (subset_ground_1 : ∀ (I : Set α), Indep_1 I → I ⊆ E_1),
  ({ E := E, Indep := Indep, indep_empty := indep_empty, indep_subset := indep_subset, indep_aug := indep_aug,
        indep_maximal := indep_maximal, subset_ground := subset_ground } =
      { E := E_1, Indep := Indep_1, indep_empty := indep_empty_1, indep_subset := indep_subset_1,
        indep_aug := indep_aug_1, indep_maximal := indep_maximal_1, subset_ground := subset_ground_1 }) =
    (E = E_1 ∧ Indep = Indep_1)
-- Lean.Parser.Term
/-- `let`-declaration that is only included in the elaborated term if variable is still there.
It is often used when building macros.
 -/
Lean.Parser.Term.let_tmp : Lean.Parser.Parser
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- This is one key identity relating infinite series to q-expansions which shows that
`∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n, n ^ k q ^n` where
`q = cexp (2 π I z)`.  -/
EisensteinSeries.qExpansion_identity : ∀ {k : ℕ},
  1 ≤ k →
    ∀ (z : UpperHalfPlane),
      ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
        (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial *
          ∑' (n : ℕ), ↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.mk : String →
  Option String →
    Option Lean.Lsp.MarkupContent →
      Option Lean.Lsp.CompletionItemKind →
        Option Lean.Lsp.InsertReplaceEdit →
          Option String →
            Option Lean.Lsp.ResolvableCompletionItemData →
              Option (Array Lean.Lsp.CompletionItemTag) → Lean.Lsp.ResolvableCompletionItem
-- Mathlib.Data.Rat.Lemmas
Rat.isSquare_intCast_iff : ∀ {z : ℤ}, IsSquare ↑z ↔ IsSquare z
-- Mathlib.Data.PEquiv
PEquiv.ofSet_eq_some_iff : ∀ {α : Type u} {s : Set α} {x : DecidablePred fun x => x ∈ s} {a b : α}, (PEquiv.ofSet s) b = some a ↔ a = b ∧ a ∈ s
-- Init.Prelude
instHXorOfXorOp : {α : Type u_1} → [XorOp α] → HXor α α α
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_one_iff : ∀ {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}}, Ordinal.IsPrincipal op 1 ↔ op 0 0 = 0
-- Mathlib.Combinatorics.Enumerative.Composition
compositionAsSetFintype : (n : ℕ) → Fintype (CompositionAsSet n)
-- Mathlib.Algebra.Group.Defs
pow_mul_comm : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), a ^ m * a ^ n = a ^ n * a ^ m
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_rci : ∀ {α β : Type u} {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] [inst_4 : LE α]
  [inst_5 : Std.PRange.UpwardEnumerable α] [inst_6 : Std.Rxi.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] [inst_8 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Rci α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Given a `PreInnerProductSpace.Core` structure on a space, one can use it to turn
the space into a pre-inner product space (i.e., `SeminormedAddCommGroup` and `InnerProductSpace`).
The `SeminormedAddCommGroup` structure is expected to already be defined with
`InnerProductSpace.ofCore.toSeminormedAddCommGroup`.  -/
InnerProductSpace.ofCore : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → (cd : PreInnerProductSpace.Core 𝕜 F) → InnerProductSpace 𝕜 F
-- Lean.SubExpr
Lean.SubExpr.Pos.fromString! : String → Lean.SubExpr.Pos
-- Lean.Meta.Eqns
/-- Runs `act` with the equation-affecting options restored to the values stored for `declName`
at definition time (or reset to their defaults if none were stored). Use this inside
`realizeConst` callbacks, which otherwise see the caller-independent `ctx.opts` rather than
the outer `getEqnsFor?` context.  -/
Lean.Meta.withEqnOptions : {α : Type} → Lean.Name → Lean.MetaM α → Lean.MetaM α
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- Mathlib.Tactic.Sat.FromLRAT
/-- `Valuation.mk [a, b, c]` is a valuation which is `a` at 0, `b` at 1 and `c` at 2, and false
everywhere else.  -/
Sat.Valuation.mk : List Prop → Sat.Valuation
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.size_eq_match_rci : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α] [Std.Rxi.LawfulHasSize α],
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 1
    | some next => next...*.size + 1
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize ISize
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.noZeroDivisors : NoZeroDivisors Ordinal.{u_4}
-- Mathlib.Geometry.Manifold.SmoothApprox
Continuous.exists_contMDiff_approx_and_eqOn : ∀ {E : Type u_1} {F : Type u_2} {H : Type u_3} {M : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I (↑⊤) M]
  [SigmaCompactSpace M] [T2Space M] {f : M → F} {ε : M → ℝ} (n : ℕ∞),
  Continuous f →
    Continuous ε →
      (∀ (x : M), 0 < ε x) →
        ∀ {S U : Set M},
          IsClosed S →
            U ∈ nhdsSet S →
              ContMDiffOn I (modelWithCornersSelf ℝ F) (↑n) f U →
                ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ Set.EqOn (⇑g) f S ∧ Function.support ⇑g ⊆ Function.support f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rcc : ∀ {m n i : ℕ}, (m...=n).toArray[i]? = if i < n + 1 - m then some (m + i) else none
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ⟶ Z) [inst_2 : CategoryTheory.IsIso f] {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.inv f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) h) =
    h
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.getChildNgen.match_1.splitter : (motive : Lean.NameGenerator × Lean.NameGenerator → Sort u_1) →
  (x : Lean.NameGenerator × Lean.NameGenerator) → ((cngen ngen : Lean.NameGenerator) → motive (cngen, ngen)) → motive x
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.mul_add_mul_eq : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R},
  A.IsDetpBalanced a b →
    ∀ (s t : ℤˣ), a * Matrix.detp s A + b * Matrix.detp t A = b * Matrix.detp s A + a * Matrix.detp t A