mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.Quotient
Quotient.finChoiceEquiv_symm_apply : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  (q : Quotient inferInstance) (i : ι), Quotient.finChoiceEquiv.symm q i = q.eval i
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- The disjoint union of two completely metrizable spaces is completely metrizable.  -/
TopologicalSpace.IsCompletelyMetrizableSpace.sum : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X]
  [inst_2 : TopologicalSpace Y] [TopologicalSpace.IsCompletelyMetrizableSpace Y],
  TopologicalSpace.IsCompletelyMetrizableSpace (X ⊕ Y)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- **Alias** of `writtenInExtChartAt_prod`. -/
writtenInExtChart_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] {I : ModelWithCorners 𝕜 E H}
  [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] [inst_7 : TopologicalSpace H']
  [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} [inst_9 : ChartedSpace H M]
  [inst_10 : ChartedSpace H' M'] {G : Type u_8} {G' : Type u_9} {F : Type u_10} {F' : Type u_11} {N : Type u_12}
  {N' : Type u_13} [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] [inst_13 : NormedAddCommGroup F']
  [inst_14 : NormedSpace 𝕜 F'] [inst_15 : TopologicalSpace G] [inst_16 : TopologicalSpace N]
  [inst_17 : TopologicalSpace G'] [inst_18 : TopologicalSpace N'] {J : ModelWithCorners 𝕜 F G}
  {J' : ModelWithCorners 𝕜 F' G'} [inst_19 : ChartedSpace G N] [inst_20 : ChartedSpace G' N'] {f : M → N} {g : M' → N'}
  {x : M} {x' : M'},
  writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) =
    Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g)
-- Init.Data.UInt.Bitwise
UInt64.ofNatLT_or : ∀ (a b : ℕ) (ha : a < 2 ^ 64) (hb : b < 2 ^ 64),
  UInt64.ofNatLT (a ||| b) ⋯ = UInt64.ofNatLT a ha ||| UInt64.ofNatLT b hb
-- Mathlib.Algebra.Group.Basic
zpow_add : ∀ {G : Type u_3} [inst : Group G] (a : G) (m n : ℤ), a ^ (m + n) = a ^ m * a ^ n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).contains k = true
-- Mathlib.Order.Hom.Basic
OrderIso.map_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α] [inst_3 : OrderBot β]
  (f : α ≃o β), f ⊥ = ⊥
-- Mathlib.Data.Finset.Insert
Finset.consPiProd_snd : ∀ {α : Type u_1} {s : Finset α} {a : α} (f : α → Type u_3) (has : a ∉ s) (x : (i : α) → i ∈ Finset.cons a s has → f i)
  (i : α) (hi : i ∈ s), (Finset.consPiProd f has x).2 i hi = x i ⋯
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A variant of `Sieve.natTransOfLe` with universe lifting.  -/
CategoryTheory.Sieve.uliftNatTransOfLe : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → {S T : CategoryTheory.Sieve X} → S ≤ T → (S.uliftFunctor ⟶ T.uliftFunctor)
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
/-- The entropy of `φ '' F` is at most the entropy of `F` if `φ` is uniformly continuous.  -/
Dynamics.coverEntropy_image_le_of_uniformContinuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : UniformSpace X] [inst_1 : UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    UniformContinuous φ → ∀ (F : Set X), Dynamics.coverEntropy T (φ '' F) ≤ Dynamics.coverEntropy S F
-- Lean.Meta.WHNF
/-- Return `some (Expr.mvar mvarId)` if metavariable `mvarId` is blocking reduction.  -/
Lean.Meta.getStuckMVar? : Lean.Expr → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Tactic.CasesM
/-- Elaborate a list of terms with holes into a list of patterns.  -/
Mathlib.Tactic.elabPatterns : Array Lean.Term → Lean.Elab.TermElabM (Array Lean.Meta.AbstractMVarsResult)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f, X + r) = (-1)^{deg f} * f(-r)`  -/
Polynomial.resultant_X_add_C_right : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (m : ℕ) (r : R),
  f.natDegree ≤ m → f.resultant (Polynomial.X + Polynomial.C r) m 1 = (-1) ^ m * Polynomial.eval (-r) f
-- Init.Data.SInt.Lemmas
Int32.lt_iff_toBitVec_slt : ∀ {a b : Int32}, a < b ↔ a.toBitVec.slt b.toBitVec = true
-- Init.Data.Vector.Basic
/-- Convert a vector to a list.  -/
Vector.toList : {α : Type u_1} → {n : ℕ} → Vector α n → List α
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_δ' : ∀ {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (i' : Fin (m + 2))
  (h : autoParam (n + j = m) SimplexCategory.δ₀Iter_δ'._auto_1),
  autoParam (↑i' = ↑i + j) SimplexCategory.δ₀Iter_δ'._auto_3 →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter j h) (SimplexCategory.δ i') =
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.δ₀Iter j ⋯)
-- Mathlib.FieldTheory.KummerExtension
X_pow_sub_C_irreducible_iff_forall_prime_of_odd : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  Odd n →
    ∀ {a : K}, Irreducible (Polynomial.X ^ n - Polynomial.C a) ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a
-- Mathlib.Algebra.Lie.Prod
LieHom.snd_apply : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (x : L₁ × L₂), (LieHom.snd R L₁ L₂) x = x.2
-- Mathlib.Geometry.Manifold.ChartedSpace
sum_chartAt_inl_apply : ∀ {H : Type u} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] {x y : M},
  ↑(chartAt H (Sum.inl x)) (Sum.inl y) = ↑(chartAt H x) y
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] (k : α)
  (f : Option (β k) → Option (β k)), m₁.Equiv m₂ → (m₁.alter k f).Equiv (m₂.alter k f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_zero : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v), w.getVert 0 = u
-- Batteries.Data.Vector.Lemmas
Vector.getElem_succ_scanl : ∀ {β : Type u_1} {α : Type u_2} {n i : ℕ} {init : β} {f : β → α → β} {as : Vector α n} (h : i + 1 < n + 1),
  (Vector.scanl f init as)[i + 1] = f (Vector.scanl f init as)[i] as[i]
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_le_maxKey?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km kmi : α},
  Std.Internal.List.maxKey? l = some km →
    (Std.Internal.List.maxKey? (Std.Internal.List.insertEntry k v l)).get ⋯ = kmi → (compare km kmi).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- The Leibniz (parametrized) adjunction `F.leibnizPushout ⊣₂ G.leibnizPullback` induced by a
parameterized adjunction `F ⊣₂ G`.  -/
CategoryTheory.Functor.leibnizAdjunction : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) →
                (F ⊣₂ G) →
                  [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] →
                    [inst_4 : CategoryTheory.Limits.HasPushouts C₃] → F.leibnizPushout ⊣₂ G.leibnizPullback
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.mk.sizeOf_spec : ∀ {α : Sort u_1} {β : Sort u_2} [inst : SizeOf α] [inst_1 : SizeOf β] (toFun : α → β) (inj' : Function.Injective toFun),
  sizeOf { toFun := toFun, inj' := inj' } = 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.prod_dite_eq`.  -/
Fintype.prod_dite_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι)
  (f : (j : ι) → i = j → M), (∏ j, if h : i = j then f j h else 1) = f i ⋯
-- Mathlib.MeasureTheory.Measure.AddContent
/-- **Alias** of `MeasureTheory.addContent_sdiff_of_ne_top`. -/
MeasureTheory.addContent_diff_of_ne_top : ∀ {α : Type u_1} {C : Set (Set α)} (m : MeasureTheory.AddContent ENNReal C),
  MeasureTheory.IsSetRing C → (∀ s ∈ C, m s ≠ ⊤) → ∀ {s t : Set α}, s ∈ C → t ∈ C → t ⊆ s → m (s \ t) = m s - m t
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- The **Four Functions Theorem** on a powerset algebra. See `four_functions_theorem` for the
finite distributive lattice generalisation.  -/
Finset.four_functions_theorem : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f₁ f₂ f₃ f₄ : Finset α → β} [ExistsAddOfLE β] (u : Finset α),
  0 ≤ f₁ →
    0 ≤ f₂ →
      0 ≤ f₃ →
        0 ≤ f₄ →
          (∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
            ∀ {𝒜 ℬ : Finset (Finset α)},
              𝒜 ⊆ u.powerset →
                ℬ ⊆ u.powerset → (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportFailure.mk.injEq : ∀ (module const : Lean.Name) (exception : Lean.Exception) (module_1 const_1 : Lean.Name) (exception_1 : Lean.Exception),
  ({ module := module, const := const, exception := exception } =
      { module := module_1, const := const_1, exception := exception_1 }) =
    (module = module_1 ∧ const = const_1 ∧ exception = exception_1)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.inhabitedCocone.eq_1 : ∀ {C : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C),
  CategoryTheory.Limits.inhabitedCocone F =
    {
      default :=
        { pt := F.obj { as := PUnit.unit },
          ι :=
            CategoryTheory.NatTrans.mk'
              (fun x =>
                match x with
                | { as := PUnit.unit } =>
                  CategoryTheory.CategoryStruct.id
                    (((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{u_1 + 1})).obj
                          (F.obj { as := PUnit.unit })).obj
                      { as := PUnit.unit }))
              ⋯ } }
-- Mathlib.Combinatorics.Configuration
Configuration.HasLines.mk : {P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      [toNondegenerate : Configuration.Nondegenerate P L] →
        (mkLine : {p₁ p₂ : P} → p₁ ≠ p₂ → L) →
          (∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ mkLine h ∧ p₂ ∈ mkLine h) → Configuration.HasLines P L
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.ext_iff : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] {𝔖 : Set (Set E)}
  {f g : UniformConvergenceCLM σ F 𝔖}, f = g ↔ ∀ (x : E), f x = g x
-- Lean.Elab.Tactic.Omega.Core
/-- Invariant between `possible` and `proveFalse?`.  -/
Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec : ∀ (self : Lean.Elab.Tactic.Omega.Problem), (self.possible || self.proveFalse?.isSome) = true
-- Init.Data.BitVec.Basic
/-- Transforms a bitvector of length `w` into a bitvector of length `v`, padding with `0` as needed.

The specific behavior depends on the relationship between the starting width `w` and the final width
`v`:
 * If `v > w`, it is zero-extended; the high bits are padded with zeroes until the bitvector has `v`
   bits.
 * If `v = w`, the bitvector is returned unchanged.
 * If `v < w`, the high bits are truncated.

`BitVec.setWidth`, `BitVec.zeroExtend`, and `BitVec.truncate` are aliases for this operation.

SMT-LIB name: `zero_extend`.
 -/
BitVec.truncate : {w : ℕ} → (v : ℕ) → BitVec w → BitVec v
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightEquiv_symm_coweightMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (n : N₂),
  (RootPairing.Equiv.coweightEquiv P Q e).symm ((↑e).coweightMap n) = n
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.maxKey?.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β),
  x.maxKey? =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => some k
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      r.maxKey?
-- Mathlib.Data.List.Sigma
List.kunion.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (x : List (Sigma β)) (s : Sigma β) (l₁ : List (Sigma β)),
  (s :: l₁).kunion x = s :: l₁.kunion (List.kerase s.fst x)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go_eq_carry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α),
  ∀ curr ≤ w,
    ∀ (cin origCin : aig.Ref) (lhs rhs : aig.RefVec w) (lhsExpr rhsExpr : BitVec w) (assign : α → Bool),
      (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := lhs.get idx hidx }⟧ = lhsExpr.getLsbD idx) →
        (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := rhs.get idx hidx }⟧ = rhsExpr.getLsbD idx) →
          ⟦assign, { aig := aig, ref := cin }⟧ =
              BitVec.carry curr lhsExpr rhsExpr ⟦assign, { aig := aig, ref := origCin }⟧ →
            ⟦assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin⟧ =
              BitVec.carry w lhsExpr rhsExpr ⟦assign, { aig := aig, ref := origCin }⟧
-- Mathlib.Data.Nat.Count
Nat.count_ne_iff_exists : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, Nat.count p n ≠ 0 ↔ ∃ m < n, p m
-- Init.Data.Int.DivMod.Lemmas
Int.sub_fmod : ∀ (a b n : ℤ), (a - b).fmod n = (a.fmod n - b.fmod n).fmod n
-- Init.Grind.ToInt
Lean.Grind.instBEqIntInterval : BEq Lean.Grind.IntInterval
-- Lean.Data.Lsp.Basic
Lean.Lsp.ChangeAnnotation.mk.injEq : ∀ (label : String) (needsConfirmation : Bool) (description? : Option String) (label_1 : String)
  (needsConfirmation_1 : Bool) (description?_1 : Option String),
  ({ label := label, needsConfirmation := needsConfirmation, description? := description? } =
      { label := label_1, needsConfirmation := needsConfirmation_1, description? := description?_1 }) =
    (label = label_1 ∧ needsConfirmation = needsConfirmation_1 ∧ description? = description?_1)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Mathlib.Meta.Positivity.log_nonneg_of_isNegNat : ∀ {e : ℝ} {n : ℕ}, Mathlib.Meta.NormNum.IsInt e (Int.negOfNat n) → 0 ≤ Real.log e
-- Lean.Data.Position
_private.Lean.Data.Position.0.Lean.FileMap.ofString.loop : String → String.Pos.Raw → Array String.Pos.Raw → Lean.FileMap
-- Mathlib.CategoryTheory.Filtered.Final
/-- The forgetful functor of the over category on any cofiltered or empty category is initial.  -/
CategoryTheory.Over.initial_forget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (c : C),
  (CategoryTheory.Over.forget c).Initial
-- Init.Prelude
/-- `False` is the empty proposition. Thus, it has no introduction rules.
It represents a contradiction. `False` elimination rule, `False.rec`,
expresses the fact that anything follows from a contradiction.
This rule is sometimes called ex falso (short for ex falso sequitur quodlibet),
or the principle of explosion.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)
 -/
False : Prop
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Imp.eq_1 : ∀ {L : FirstOrder.Language} {α : Type w} {n : ℕ} (T : L.Theory) (φ ψ : L.BoundedFormula α n), T.Imp φ ψ = T ⊨ᵇ φ.imp ψ
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_congr : ∀ {u v : ℕ → ENNReal}, u =ᶠ[Filter.atTop] v → ExpGrowth.expGrowthInf u = ExpGrowth.expGrowthInf v
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.Limits.spanExt.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX iX_1 : X ≅ X') (e_iX : iX = iX_1)
  (iY iY_1 : Y ≅ Y') (e_iY : iY = iY_1) (iZ iZ_1 : Z ≅ Z') (e_iZ : iZ = iZ_1) {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'}
  {g' : X' ⟶ Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  CategoryTheory.Limits.spanExt iX iY iZ wf wg = CategoryTheory.Limits.spanExt iX_1 iY_1 iZ_1 ⋯ ⋯
-- Mathlib.Order.Filter.Pointwise
Filter.pure_zero : ∀ {α : Type u_2} [inst : Zero α], pure 0 = 0
-- Init.Data.List.Lemmas
List.filterMap.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → Option β), List.filterMap f [] = []
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instElemOrbit_1.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (x : AddAction.orbitRel.Quotient G α),
  AddAction.instElemOrbit_1 x =
    { vadd := fun g => Set.MapsTo.restrict (fun x => g +ᵥ x) x.orbit x.orbit ⋯, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.liftPrincipalSeg_top : Ordinal.liftPrincipalSeg.top = Ordinal.univ.{u, v}
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Choice.mk.inj : ∀ {cnstrs : List Lean.Meta.Grind.EMatch.Cnstr} {gen : ℕ} {assignment : Array Lean.Expr}
  {sources : Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode} {cnstrs_1 : List Lean.Meta.Grind.EMatch.Cnstr} {gen_1 : ℕ}
  {assignment_1 : Array Lean.Expr} {sources_1 : Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode},
  { cnstrs := cnstrs, gen := gen, assignment := assignment, sources := sources } =
      { cnstrs := cnstrs_1, gen := gen_1, assignment := assignment_1, sources := sources_1 } →
    cnstrs = cnstrs_1 ∧ gen = gen_1 ∧ assignment = assignment_1 ∧ sources = sources_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH1.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.shortComplexH1 A =
    { X₁ := ModuleCat.of k (G × G →₀ ↑A), X₂ := ModuleCat.of k (G →₀ ↑A), X₃ := ModuleCat.of k ↑A,
      f := groupHomology.d₂₁ A, g := groupHomology.d₁₀ A, zero := ⋯ }
-- Mathlib.RingTheory.PicardGroup
/-- If a flat `R`-module becomes free of rank 1 after base-changing to a faithful `R`-algebra `A`,
then it embeds into `A`.  -/
Module.Flat.toAlgebra : {R : Type u} →
  {M : Type v} →
    {A : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring A] → [inst_4 : Algebra R A] → (TensorProduct R A M ≃ₗ[A] A) → M →ₗ[R] A
-- Mathlib.Topology.Connected.Basic
preconnectedSpace_iff_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α], PreconnectedSpace α ↔ ∀ (x : α), connectedComponent x = Set.univ
-- Mathlib.RingTheory.Ideal.Operations
Submodule.coe_mapAlgEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_3} {B : Type u_4} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B) (a : Submodule R B),
  ↑((Submodule.mapAlgEquiv f).symm a) = ⇑f.symm '' ↑a
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is any function and `g` is analytic without zero on `U`, then `f` is
meromorphic in normal form on `U` iff `g • f` is meromorphic in normal form on
`U`.
 -/
meromorphicNFOn_smul_iff_right_of_analyticOnNhd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} {g : 𝕜 → 𝕜},
  AnalyticOnNhd 𝕜 g U → (∀ u ∈ U, g u ≠ 0) → (MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U)
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.public.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
_private.Mathlib.LinearAlgebra.FreeModule.Finite.Matrix.0.linearMapEquivFun : (R : Type u) →
  (S : Type u') →
    (M : Type v) →
      (N : Type w) →
        [inst : Ring R] →
          [inst_1 : Ring S] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : Module.Free R M] →
                  [inst_5 : AddCommGroup N] →
                    [inst_6 : Module R N] →
                      [inst_7 : Module S N] →
                        [inst_8 : SMulCommClass R S N] → (M →ₗ[R] N) ≃ₗ[S] Module.Free.ChooseBasisIndex R M → N
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.Monoidal.tensorObj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (PresheafOfModules.Monoidal.tensorObj M₁ M₂).obj X =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (M₁.obj X) (M₂.obj X)
-- Init.Data.List.Sublist
List.cons_subset : ∀ {α : Type u_1} {a : α} {l m : List α}, a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfc_complex_eq_real : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : ContinuousFunctionalCalculus ℂ A IsStarNormal] [T2Space A] {f : ℂ → ℂ} (a : A),
  (∀ x ∈ spectrum ℂ a, star (f x) = f x) →
    autoParam (IsSelfAdjoint a) cfc_complex_eq_real._auto_1 → cfc f a = cfc (fun x => (f ↑x).re) a
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Icc a b` and antitone on `Ici b`, then the maximum of `f` on `Ici a` is
attained at `b`.  -/
isMaxOn_Ici_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  MonotoneOn f (Set.Icc a b) → AntitoneOn f (Set.Ici b) → IsMaxOn f (Set.Ici a) b
-- Init.Grind.AC
Lean.Grind.AC.eq_erase0_rhs : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (lhs rhs rhs' : Lean.Grind.AC.Seq),
  rhs.erase0.beq' rhs' = true →
    Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs'
-- Batteries.Util.Cache
/-- Access the cache. Calling this function for the first time will initialize the cache
with the function provided in the constructor.
 -/
Batteries.Tactic.Cache.get : {α : Type} → Batteries.Tactic.Cache α → Lean.MetaM α
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAt.mem_domChart_source : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x), x ∈ h.domChart.source
-- Lean.Parser.Extra
Lean.Parser.optional.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev.congr_simp : ∀ {s : String} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.startPos), pos.prev h = pos_1.prev ⋯